diff --git a/echo_mio.sh b/echo_mio.sh new file mode 100755 index 00000000..e18dcb6e --- /dev/null +++ b/echo_mio.sh @@ -0,0 +1,2 @@ +#!/bin/sh +exec dune exec --display=quiet --profile=release "examples/echo_mio.exe" -- $@