author | wenzelm |
Tue, 03 Jan 2017 23:21:09 +0100 | |
changeset 64770 | 1ddc262514b8 |
parent 64769 | 6be5ec46688f |
child 64772 | 346d5158fc2f |
child 64773 | 223b2ebdda79 |
child 64775 | dd3797f1e0d6 |
--- 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