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.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 84df3ecd..b2072221 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -119,7 +119,7 @@ let schedule_vio_compilation j fs =
let rec filter_argv b = function
| [] -> []
| "-schedule-vio2vo" :: 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 prog = Sys.argv.(0) in