diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 7e402d006647..370e8f7d4a5a 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -226,7 +226,7 @@ protected def list : CliM PUnit := do IO.println script.name protected nonrec def run : CliM PUnit := do - processOptions lakeOption + processLeadingOptions lakeOption -- between `lake [script] run` and `` let config ← mkLoadConfig (← getThe LakeOptions) let ws ← loadWorkspace config if let some spec ← takeArg? then diff --git a/src/lake/examples/scripts/expected.out b/src/lake/examples/scripts/expected.out index 47508d273a14..ac7cdad5a4da 100644 --- a/src/lake/examples/scripts/expected.out +++ b/src/lake/examples/scripts/expected.out @@ -3,6 +3,7 @@ scripts/dismiss scripts/greet Hello, world! Hello, me! +Hello, --me! Display a greeting USAGE: diff --git a/src/lake/examples/scripts/test.sh b/src/lake/examples/scripts/test.sh index b032172cc365..0d90532679c3 100755 --- a/src/lake/examples/scripts/test.sh +++ b/src/lake/examples/scripts/test.sh @@ -11,6 +11,7 @@ $LAKE update $LAKE script list | tee produced.out $LAKE run /greet | tee -a produced.out $LAKE script run greet me | tee -a produced.out +$LAKE script run greet --me | tee -a produced.out $LAKE script doc greet | tee -a produced.out $LAKE script run hello | tee -a produced.out $LAKE script run dep/hello | tee -a produced.out