helper script to run benchs

c-cube · c-cube · commit c299b3230967 · 2024-05-13T21:05:55.000-04:00
diff --git a/benchs/run_benchs.sh b/benchs/run_benchs.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+exec dune exec --profile=release benchs/run_benchs.exe -- $@

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+#!/bin/sh`
	`2`	`+`
	`3`	`+exec dune exec --profile=release benchs/run_benchs.exe -- $@`