From 10fa0c0b6b6d29901de9258d7fad402e3b6ec79a Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 30 May 2008 10:13:59 +0000 Subject: - Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t" n'étaient pas gérés, merci à Julien). - Correction pb blocage CoqIDE quand le browser n'est pas déja lancé (utilisation pour cela de Sys.command au lieu de Unix.open_process_full). - MAJ CHANGES et COMPATIBILITY. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/flags.ml | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index f9c855d86e..0635ad7c1f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -112,18 +112,14 @@ let boxed_definitions _ = !boxed_definitions let subst_command_placeholder s t = let buff = Buffer.create (String.length s + String.length t) in - 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 i = ref 0 in + while (!i < String.length s) do + if s.[!i] = '%' & !i+1 < String.length s & 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 let browser_cmd_fmt = try -- cgit v1.2.3