File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -301,6 +301,8 @@ def ShellOptions.process (opts : ShellOptions)
301301 let arg ← checkOptArg "j" optArg?
302302 let some numThreads := arg.toNat?
303303 | throwExpectedNumeric "j"
304+ if numThreads == 0 then
305+ throwExpectedPositive "j"
304306 if h : numThreads < UInt32.size then
305307 let numThreads := UInt32.ofNatLT numThreads h
306308 let forwardedArgs := opts.forwardedArgs.push s! "-j{ arg} " ;
@@ -460,6 +462,9 @@ where
460462 @[inline] throwExpectedNumeric opt := do
461463 eprint s! "error: expected numeric argument for option '-{ opt} '\n "
462464 throw 1
465+ @[inline] throwExpectedPositive opt := do
466+ eprint s! "error: expected positive numeric argument for option '-{ opt} '\n "
467+ throw 1
463468 @[inline] throwTooLarge opt := do
464469 eprint s! "error: argument value for '-{ opt} ' is too large\n "
465470 throw 1
Original file line number Diff line number Diff line change 1+ set -euo pipefail
2+
3+ out=" ${NAME} .out"
4+ trap ' rm -f "$out"' EXIT
5+
6+ if lean -j0 > " $out " 2>&1 ; then
7+ echo " lean -j0 unexpectedly succeeded" >&2
8+ exit 1
9+ fi
10+
11+ grep -Fx " error: expected positive numeric argument for option '-j'" " $out "
You can’t perform that action at this time.
0 commit comments