src/Pure/General/url.scala
changeset 64766 6fd05caf55f0
parent 64759 100941134718
child 64775 dd3797f1e0d6
--- a/src/Pure/General/url.scala	Tue Jan 03 17:33:08 2017 +0100
+++ b/src/Pure/General/url.scala	Tue Jan 03 19:22:17 2017 +0100
@@ -81,8 +81,6 @@
     if (name.startsWith("file://")) name
     else {
       val s = name.replaceAll(" ", "%20")
-      if (!Platform.is_windows) "file://" + s
-      else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
-      else "file:///" + s.replace('\\', '/')
+      "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s)
     }
 }