author | wenzelm |
Tue, 03 Jan 2017 14:45:50 +0100 | |
changeset 64760 | 8c1557308eb5 |
parent 64759 | 100941134718 |
child 64761 | ae97a5afffcc |
--- 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('\\', '/')