src/Tools/jEdit/src/jedit_lib.scala
changeset 60992 89effcb342df
parent 60988 1d7a7e33fd67
child 61192 98eba31c51f8
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 20:36:06 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 20 21:08:47 2015 +0200
@@ -308,7 +308,7 @@
   {
     val name1 =
       if (name.startsWith("idea-icons/")) {
-        val file = File.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
+        val file = File.platform_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
         "jar:" + file + "!/" + name
       }
       else name