aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-08 21:12:09 +0200
committerHugo Herbelin2019-05-14 11:14:59 +0200
commitd452f359566ec6593aad564acb281f5a49dd931a (patch)
treef4aef5c67137a8120c7d7ddfeec2e72165cc40fb
parent9f11eeefc204bdad029b66f30bc6c52377af63ae (diff)
Option -check-vio-tasks: fail gracefully when not finding expected integers.
-rw-r--r--toplevel/coqcargs.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 7445619d26..c3f099869c 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -82,7 +82,14 @@ let set_vio_checking_j opts opt j =
prerr_endline "setting the J variable like in 'make vio2vo J=3'";
exit 1
-let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
+let get_task_list s =
+ List.map (fun s ->
+ try int_of_string s
+ with Failure _ ->
+ prerr_endline "Option -check-vio-tasks expects a comma-separated list";
+ prerr_endline "of integers followed by a list of files";
+ exit 1)
+ (Str.split (Str.regexp ",") s)
let is_not_dash_option = function
| Some f when String.length f > 0 && f.[0] <> '-' -> true