more robust, notably on Windows;
authorwenzelm
Tue, 03 Jan 2017 23:21:09 +0100
changeset 64770 1ddc262514b8
parent 64769 6be5ec46688f
child 64772 346d5158fc2f
child 64773 223b2ebdda79
child 64775 dd3797f1e0d6
more robust, notably on Windows;
src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Jan 03 22:07:14 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Jan 03 23:21:09 2017 +0100
@@ -320,7 +320,7 @@
   {
     val name1 =
       if (name.startsWith("idea-icons/")) {
-        val file = Url.platform_file(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
+        val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString
         "jar:" + file + "!/" + name
       }
       else name