From 92579449f62f0fd7699b0b447f3aee0d82d1b5c3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 23 Feb 2017 13:48:47 +0100
Subject: [safe-string] tools

No functional changes.
---
 tools/coq_makefile.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'tools/coq_makefile.ml')

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";
-- 
cgit v1.2.3