debug subst_command_placeholder : replace %s and not only %

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

1 files changed, 5 insertions, 3 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 36179bc8a..3c3d6ceb8 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -112,9 +112,11 @@ let boxed_definitions _ = !boxed_definitions
 
 let subst_command_placeholder s t =
   let buff = Buffer.create (String.length s + String.length t) in
-  for i = 0 to String.length s - 2 do
-    if s.[i] = '%' & s.[i+1] = 's' then Buffer.add_string buff t
-    else Buffer.add_char buff s.[i]
+  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