changeset 64770 | 1ddc262514b8 |
parent 64730 | 76996d915894 |
child 64824 | 330ec9bc4b75 |
--- 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