aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-02-23 13:48:47 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-14 22:19:27 +0100
commit92579449f62f0fd7699b0b447f3aee0d82d1b5c3 (patch)
treed4e92bb8b814467be59ee8a7de91bec4b3cabcec /tools/coq_makefile.ml
parentfacf0520a47603d2679508136cbed43def0744cc (diff)
[safe-string] tools
No functional changes.
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml7
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";