more basic Windows path operations -- evade exception InvalidArc with Unicode;
authorwenzelm
Tue, 08 Sep 2015 21:10:23 +0200
changeset 61137 4010e1559a24
parent 61136 168f84f45730
child 61138 dcbec1b22b07
more basic Windows path operations -- evade exception InvalidArc with Unicode;
src/Pure/ML-Systems/windows_path.ML
--- a/src/Pure/ML-Systems/windows_path.ML	Tue Sep 08 20:06:17 2015 +0200
+++ b/src/Pure/ML-Systems/windows_path.ML	Tue Sep 08 21:10:23 2015 +0200
@@ -13,11 +13,10 @@
             (case Char.fromString drive of
               NONE => drive ^ ":"
             | SOME d => String.str (Char.toUpper d) ^ ":");
-        in OS.Path.toString {vol = vol, arcs = arcs, isAbs = true} end
+        in String.concatWith "\\" (vol :: arcs) end
     | arcs =>
         (case OS.Process.getEnv "CYGWIN_ROOT" of
-          SOME root =>
-            OS.Path.concat (root, OS.Path.toString {vol = "", arcs = arcs, isAbs = false})
+          SOME root => OS.Path.concat (root, String.concatWith "\\" arcs)
         | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT"))
   else String.translate (fn #"/" => "\\" | c => String.str c) path;