diff options
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r-- | tools/coq_makefile.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4842a8915..23479aee5 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -125,12 +125,9 @@ let physical_dir_of_logical_dir ldir = let le = String.length ldir - 1 in let pdir = if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) - else String.copy ldir + else ldir in - for i = 0 to le - 1 do - if pdir.[i] = '.' then pdir.[i] <- '/'; - done; - pdir + String.map (fun c -> if c = '.' then '/' else c) pdir let standard opt = print "byte:\n"; |