# HG changeset patch
# User wenzelm
# Date 1483451150 -3600
# Node ID 8c1557308eb5999e731b876ff352132eb45eff8f
# Parent  100941134718c7de39e0687a67c7ee0aa5484d79
more liberal drive letter, for the sake of file:// URLs;

diff -r 100941134718 -r 8c1557308eb5 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('\\', '/')