debug : case where length of s is < 2...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11005 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 7 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 3c3d6ceb83..f9c855d86e 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -112,13 +112,18 @@ let boxed_definitions _ = !boxed_definitions
 
 let subst_command_placeholder s t =
   let buff = Buffer.create (String.length s + String.length t) in
-  let i = ref 0 in
-  while (!i <> String.length s - 2) do
-    if s.[!i] = '%' & s.[!i+1] = 's' then (Buffer.add_string buff t;incr i)
-    else Buffer.add_char buff s.[!i];
-    incr i
-  done;
-  Buffer.contents buff
+    if String.length s < 2 then
+      Buffer.add_string buff s
+    else
+      begin
+	let i = ref 0 in
+	  while (!i <= String.length s - 2) do
+	    if s.[!i] = '%' & s.[!i+1] = 's' then (Buffer.add_string buff t;incr i)
+	    else Buffer.add_char buff s.[!i];
+	    incr i
+	  done
+      end;
+    Buffer.contents buff
 
 let browser_cmd_fmt =
  try