1 files changed, 5 insertions, 0 deletions
diff --git a/Omni/Ide/repl.sh b/Omni/Ide/repl.sh
index 3b6a536..d4ff200 100755
--- a/Omni/Ide/repl.sh
+++ b/Omni/Ide/repl.sh
@@ -10,6 +10,7 @@
 ###
 ### Options:
 ###   --bash   start bash instead of the target language repl
+###   --cmd x  run 'x' instead of bash, or the target language repl
 help() {
     sed -rn 's/^### ?//;T;p' "$0"
 }
@@ -23,6 +24,10 @@ fi
   if [[ "$1" == "--bash" ]]; then
     CMD="bash"
     shift
+  elif [[ "$1" == "--cmd" ]]; then
+    shift
+    CMD="$1"
+    shift
   fi
   targets="${*:?}"
   json=$(bild --plan "${targets[@]}")