| 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