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