--- 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