diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean index d5cbdc0cd8..d424a79fb6 100644 --- a/src/Lean/Shell.lean +++ b/src/Lean/Shell.lean @@ -166,7 +166,7 @@ def displayHelp (useStderr : Bool) : IO Unit := do out.putStrLn " -s, --tstack=num thread stack size in Kb" out.putStrLn " --server start lean in server mode" out.putStrLn " --worker start lean in server-worker mode" - out.putStrLn " --plugin=file[:fn] load and initialize Lean shared library for registering linters etc." + out.putStrLn " --plugin=file[=fn] load and initialize Lean shared library for registering linters etc." out.putStrLn " --load-dynlib=file load shared library to make its symbols available to the interpreter" out.putStrLn " --setup=file JSON file with module setup data (supersedes the file's header)" out.putStrLn " --json report Lean output (e.g., messages) as JSON (one per line)" @@ -410,10 +410,10 @@ def ShellOptions.process (opts : ShellOptions) Internal.enableDebug arg return opts -- if not `LEAN_DEBUG`, fall through to unknown option - | 'p' => -- `--plugin=file[:fn]` + | 'p' => -- `--plugin=file[=fn]` let arg ← checkOptArg "p" optArg? let (path, fn?) := - let pos := arg.find ':' + let pos := arg.find '=' if h : pos.IsAtEnd then (FilePath.mk arg, none) else diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..f32b664dfb 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// dear bot, please update stage0 #include "util/options.h" namespace lean { diff --git a/tests/pkg/user_plugin/run_test.sh b/tests/pkg/user_plugin/run_test.sh index 6b25f1a12d..bba6f1ba20 100644 --- a/tests/pkg/user_plugin/run_test.sh +++ b/tests/pkg/user_plugin/run_test.sh @@ -58,7 +58,7 @@ echo "Testing plugin load with a provided initialization function ..." INIT_PLUGIN=.lake/libUserPlugin.$SHLIB_EXT INIT_PLUGIN_FN=initialize_${PKG}_UserPlugin cp $PLUGIN $INIT_PLUGIN -echo | lean --plugin=$INIT_PLUGIN:$INIT_PLUGIN_FN --stdin 2>&1 | diff <(echo "$EXPECTED_OUT") - +echo | lean --plugin=$INIT_PLUGIN=$INIT_PLUGIN_FN --stdin 2>&1 | diff <(echo "$EXPECTED_OUT") - # Print success echo "Tests completed successfully."