make just ./miri print help text without 'unknown command'

2024-11-24 15:54:15 +00:00 · 2020-04-06 09:34:27 +02:00 · 2020-04-06 09:34:27 +02:00 · 3554f54173
commit 3554f54173
parent 86c57a8490
1 changed files with 4 additions and 2 deletions
--- a/6
+++ b/6
@ -141,8 +141,10 @@ run|run-debug)
    exec cargo run $CARGO_BUILD_FLAGS -- --sysroot "$MIRI_SYSROOT" "$@"
    ;;
 *)
-    echo "Unknown command: $COMMAND"
-    echo
+    if [ -n "$COMMAND" ]; then
+      echo "Unknown command: $COMMAND"
+      echo
+    fi
    echo "$USAGE"
    exit 1
 esac