# HG changeset patch # User wenzelm # Date 1620471990 -7200 # Node ID d5c3eee7da7476c89ab4a074877526a4f431baf9 # Parent 4fbbf421c376734bf84cb20848e78382f0699665 separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597); diff -r 4fbbf421c376 -r d5c3eee7da74 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sat May 08 00:31:51 2021 +0200 +++ b/Admin/components/components.sha1 Sat May 08 13:06:30 2021 +0200 @@ -92,6 +92,7 @@ 7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz +989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz 20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz 736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz 9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz diff -r 4fbbf421c376 -r d5c3eee7da74 Admin/components/main --- a/Admin/components/main Sat May 08 00:31:51 2021 +0200 +++ b/Admin/components/main Sat May 08 13:06:30 2021 +0200 @@ -6,6 +6,7 @@ cvc4-1.8 e-2.5-1 flatlaf-1.0 +idea-icons-20210508 isabelle_fonts-20210322 jdk-15.0.2+7 jedit_build-20210201 diff -r 4fbbf421c376 -r d5c3eee7da74 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sat May 08 00:31:51 2021 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sat May 08 13:06:30 2021 +0200 @@ -264,7 +264,6 @@ "kappalayout.jar" "Navigator.jar" "SideKick.jar" - "idea-icons.jar" "jsr305-2.0.0.jar" ) diff -r 4fbbf421c376 -r d5c3eee7da74 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Sat May 08 00:31:51 2021 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sat May 08 13:06:30 2021 +0200 @@ -301,7 +301,7 @@ { val name1 = if (name.startsWith("idea-icons/")) { - val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString + val file = Path.explode("$ISABELLE_IDEA_ICONS").file.toURI.toASCIIString "jar:" + file + "!/" + name } else name