# HG changeset patch
# User wenzelm
# Date 1350740740 -7200
# Node ID fc2e3b9d485265fd54f755af6eced661557bce88
# Parent  6770da31efd8b5285000237b8f3cf0484b55355a
avoid duplicate build of jars_fresh;

diff -r 6770da31efd8 -r fc2e3b9d4852 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 20 12:01:20 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 20 15:45:40 2012 +0200
@@ -92,7 +92,6 @@
 
 BUILD_ONLY=false
 BUILD_JARS="jars"
-FRESH_OPTION=""
 JEDIT_SESSION_DIRS=""
 JEDIT_LOGIC="$ISABELLE_LOGIC"
 JEDIT_PRINT_MODE=""
@@ -117,7 +116,6 @@
         fi
         ;;
       f)
-        FRESH_OPTION="-f"
         BUILD_JARS="jars_fresh"
         ;;
       j)
@@ -166,11 +164,14 @@
 
 ## dependencies
 
-[ -e "$ISABELLE_HOME/Admin/build" ] && \
-  {
+if [ -e "$ISABELLE_HOME/Admin/build" ]; then
+  if [ "$BUILD_JARS" = jars_fresh ]; then
+    "$ISABELLE_TOOL" graphview -b -f || exit $?
+  else
     "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
-    "$ISABELLE_TOOL" graphview -b $FRESH_OPTION || exit $?
-  }
+    "$ISABELLE_TOOL" graphview -b || exit $?
+  fi
+fi
 
 PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
 GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"