# HG changeset patch
# User wenzelm
# Date 1578910711 -3600
# Node ID 85274743f789818f644abf3ec75748e04d672a6e
# Parent  1c4ec697bee5391cb2cd3b2823453cc726c13296
clarified option -f: avoid accidental target_clean for proper release snapshot;

diff -r 1c4ec697bee5 -r 85274743f789 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Jan 12 23:29:35 2020 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Jan 13 11:18:31 2020 +0100
@@ -141,7 +141,7 @@
 # options
 
 BUILD_ONLY=false
-BUILD_JARS="jars"
+FRESH_BUILD=""
 ML_PROCESS_POLICY=""
 JEDIT_LOGIC_ANCESTOR=""
 JEDIT_LOGIC_REQUIREMENTS=""
@@ -185,7 +185,7 @@
         fi
         ;;
       f)
-        BUILD_JARS="jars_fresh"
+        FRESH_BUILD="true"
         ;;
       j)
         ARGS["${#ARGS[@]}"]="$OPTARG"
@@ -242,7 +242,14 @@
 
 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   isabelle browser -b || exit $?
-  "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
+  if [ -n "$FRESH_BUILD" ]; then
+    "$ISABELLE_HOME/Admin/build" jars_fresh || exit $?
+  else
+    "$ISABELLE_HOME/Admin/build" jars || exit $?
+  fi
+elif [ -n "$FRESH_BUILD" ]; then
+  echo >&2 "### Ignoring fresh build option: not a repository clone"
+  FRESH_BUILD=""
 fi
 
 JEDIT_BUILD_JAR="$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"
@@ -288,7 +295,7 @@
   rm -rf "$ISABELLE_HOME/$TARGET_DIR"
 }
 
-[ "$BUILD_JARS" = jars_fresh ] && target_clean
+[ -n "$FRESH_BUILD" ] && target_clean
 
 
 ## build