aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornotin2009-11-19 12:45:20 +0000
committernotin2009-11-19 12:45:20 +0000
commit9a22ebe1d46b8f00980941ea0f54532595757f4e (patch)
tree8d05610971657eece1af10e2e013e3f4f6555657
parent10cd48958553133115d0d95b1c9bdc0810aee576 (diff)
Correction du bug #2118 (Coqdep does not escape #)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12536 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/coqdep_common.ml22
1 files changed, 20 insertions, 2 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 21fc66fc68..8756d864d1 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -217,11 +217,29 @@ let traite_fichier_mllib md ext =
(!a_faire, !a_faire_opt)
with Sys_error _ -> ("","")
+let escape escaped_chars s =
+ let n = ref 0 in
+ for i = 0 to String.length s - 1 do
+ n := !n +
+ (if List.mem s.[i] escaped_chars then 2 else 1)
+ done;
+ if !n = String.length s then s else
+ begin
+ let s' = String.create !n in
+ n := 0;
+ for i = 0 to String.length s - 1 do
+ if List.mem s.[i] escaped_chars then begin s'.[!n] <- '\\'; incr n end;
+ s'.[!n] <- s.[i];
+ incr n
+ done;
+ s'
+ end
+
let canonize f =
let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
match List.filter (fun (_,full) -> f' = full) !vAccu with
- | (f,_) :: _ -> f
- | _ -> f
+ | (f,_) :: _ -> escape ['#'] f
+ | _ -> escape ['#'] f
let traite_fichier_Coq verbose f =
try