src/Tools/jEdit/lib/Tools/jedit
changeset 74038 b4f57bfe82e7
parent 74017 b4e6b82fdb9e
child 75291 e4d6b9bd5071
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Jul 17 23:09:54 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Jul 18 12:48:31 2021 +0200
@@ -55,7 +55,7 @@
 # options
 
 BUILD_ONLY=false
-FRESH_BUILD=""
+BUILD_OPTIONS=""
 ML_PROCESS_POLICY=""
 JEDIT_LOGIC_ANCESTOR=""
 JEDIT_LOGIC_REQUIREMENTS=""
@@ -99,7 +99,7 @@
         fi
         ;;
       f)
-        FRESH_BUILD="true"
+        BUILD_OPTIONS="-f"
         ;;
       j)
         ARGS["${#ARGS[@]}"]="$OPTARG"
@@ -154,11 +154,7 @@
 
 ## main
 
-if [ -n "$FRESH_BUILD" ]; then
-  isabelle_scala_build fresh || exit "$?"
-else
-  isabelle_scala_build || exit "$?"
-fi
+isabelle scala_build $BUILD_OPTIONS || exit $?
 
 if [ "$BUILD_ONLY" = false ]
 then