equal
deleted
inserted
replaced
79 |
79 |
80 def platform_file(name: String): String = |
80 def platform_file(name: String): String = |
81 if (name.startsWith("file://")) name |
81 if (name.startsWith("file://")) name |
82 else { |
82 else { |
83 val s = name.replaceAll(" ", "%20") |
83 val s = name.replaceAll(" ", "%20") |
84 if (!Platform.is_windows) "file://" + s |
84 "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s) |
85 else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/') |
|
86 else "file:///" + s.replace('\\', '/') |
|
87 } |
85 } |
88 } |
86 } |