| changeset 56764 | 5b6f4655e2f2 |
| parent 56664 | 8ff8e5d00115 |
| child 56879 | ee2b61f37ad9 |
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Apr 27 13:35:18 2014 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Apr 27 19:32:55 2014 +0200 @@ -202,7 +202,6 @@ fi PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar" -GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/Graphview.jar" pushd "$JEDIT_HOME" >/dev/null || failed