diff -r 8ae1af3f88b1 -r 6fd05caf55f0 src/Pure/General/url.scala --- 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) } }