avoid duplicate build of jars_fresh;
authorwenzelm
Sat, 20 Oct 2012 15:45:40 +0200
changeset 49953 fc2e3b9d4852
parent 49952 6770da31efd8
child 49954 44658062d822
avoid duplicate build of jars_fresh;
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"