From a56dd0ec65fb3a099aeb613f6c5fa180fb4595a7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 6 Sep 2024 17:19:56 -0400 Subject: [PATCH] add echo_mio.sh --- echo_mio.sh | 2 ++ 1 file changed, 2 insertions(+) create mode 100755 echo_mio.sh 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" -- $@