src/Pure/System/standard_system.scala
changeset 36136 89b1a136edef
parent 36015 6111de7c916a
child 36193 067a01827fca
--- a/src/Pure/System/standard_system.scala	Wed Apr 14 22:07:01 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Wed Apr 14 22:08:47 2010 +0200
@@ -162,6 +162,7 @@
   /* jvm_path */
 
   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
+  private val Named_Root = new Regex("//+([^/]*)(.*)")
 
   def jvm_path(posix_path: String): String =
     if (Platform.is_windows) {
@@ -171,6 +172,11 @@
           case Cygdrive(drive, rest) =>
             result_path ++= (drive + ":" + File.separator)
             rest
+          case Named_Root(root, rest) =>
+            result_path ++= File.separator
+            result_path ++= File.separator
+            result_path ++= root
+            rest
           case path if path.startsWith("/") =>
             result_path ++= platform_root
             path