# HG changeset patch
# User wenzelm
# Date 1357329333 -3600
# Node ID a3ec244186cd6d2f10139c25b61f64e68e48556a
# Parent  e7b2cfcef94c55e673147b9c27e291df02cfd5d2
actually install required copy of Highlight.jar;

diff -r e7b2cfcef94c -r a3ec244186cd 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"