update gen-output to use native_instrs by default

diff --git a/gen-output.sh b/gen-output.sh
index 2dc1f9709424cf5355860a654a3f27b637cfc017..5a81968307a4676fcf6d457a7bd05d81c1797efb 100755 (executable)
--- a/gen-output.sh
+++ b/gen-output.sh
@@ -1,2 +1,19 @@
 #!/bin/bash
-exec cargo run > "output-for-`git describe`.json"
+case "$1" in
+    --model-only)
+        args=()
+        ;;
+    -h|--help)
+        echo "usage: $0 [--model-only] [-h|--help]"
+        exit
+        ;;
+    '')
+        args=("--features=native_instrs")
+        ;;
+    *)
+        echo "invalid option; use --help for help" >&2
+        exit 1
+        ;;
+esac
+exec cargo run "${args[@]}" > "output-for-`git describe`.json"
+