Merge PR #9541: [stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)

Reviewed-by: ejgallego

1 files changed, 6 insertions, 1 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index b549f22119..1e1a74209f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -311,8 +311,13 @@ let parse_args ~help ~init arglist : t * string list =
       }}
 
     |"-async-proofs-tac-j" ->
+      let j = get_int opt (next ()) in
+      if j <= 0 then begin
+        prerr_endline ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1");
+        exit 1;
+      end;
       { oval with stm_flags = { oval.stm_flags with
-        Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ()))
+        Stm.AsyncOpts.async_proofs_n_tacworkers = j
       }}
 
     |"-async-proofs-worker-priority" ->