summaryrefslogtreecommitdiff
path: root/stm/vio_checking.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/vio_checking.ml')
-rw-r--r--stm/vio_checking.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 06bf955c..d4dcf72c 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -43,7 +43,7 @@ let schedule_vio_checking j fs =
let rec filter_argv b = function
| [] -> []
| "-schedule-vio-checking" :: rest -> filter_argv true rest
- | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+ | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest)
| _ :: rest when b -> filter_argv b rest
| s :: rest -> s :: filter_argv b rest in
let pack = function