| 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) } }