actually install required copy of Highlight.jar;
authorwenzelm
Fri, 04 Jan 2013 20:55:33 +0100
changeset 50729 a3ec244186cd
parent 50728 e7b2cfcef94c
child 50730 883963f45ac9
actually install required copy of Highlight.jar;
src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Jan 04 20:42:09 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Jan 04 20:55:33 2013 +0100
@@ -203,6 +203,7 @@
 JEDIT_JARS=(
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar"
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"