more liberal drive letter, for the sake of file:// URLs;
authorwenzelm
Tue, 03 Jan 2017 14:45:50 +0100
changeset 64760 8c1557308eb5
parent 64759 100941134718
child 64761 ae97a5afffcc
more liberal drive letter, for the sake of file:// URLs;
src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Jan 03 14:17:03 2017 +0100
+++ b/src/Pure/General/file.scala	Tue Jan 03 14:45:50 2017 +0100
@@ -33,7 +33,7 @@
     if (Platform.is_windows) {
       val Platform_Root = new Regex("(?i)" +
         Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
-      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
+      val Drive = new Regex("""\\?([a-zA-Z]):\\*(.*)""")
 
       platform_path.replace('/', '\\') match {
         case Platform_Root(rest) => "/" + rest.replace('\\', '/')