From 32a295c7390dd40807a2154b54758c61df9b209f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Feb 2015 12:13:22 +0100
Subject: Fix bug #4014.

---
 stm/vio_checking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index 84df3ecd5e..b207222117 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  
-- 
cgit v1.2.3