From 71487a1b2b031cf6599ad90c8f834e9947220fc8 Mon Sep 17 00:00:00 2001
From: jnarboux
Date: Mon, 26 May 2008 15:50:17 +0000
Subject: 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
---
 lib/flags.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/lib/flags.ml b/lib/flags.ml
index 36179bc8ab..3c3d6ceb83 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
 
-- 
cgit v1.2.3