proper build for fresh target directory (amending d9823224fcfe);
authorwenzelm
Mon, 10 May 2021 22:32:02 +0200
changeset 73917 8b3e672df28c
parent 73916 ff716ecb0805
child 73918 fecfb96474ca
child 73921 9ab1d5fa84d0
proper build for fresh target directory (amending d9823224fcfe);
src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon May 10 22:18:12 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon May 10 22:32:02 2021 +0200
@@ -256,10 +256,13 @@
 TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum"
 
 declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
-for DEP in "$TARGET_DIR"/jars/*.jar
-do
-  TARGET_DEPS["${#TARGET_DEPS[@]}"]="$DEP"
-done
+
+if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
+  for DEP in "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION"/jars/*.jar
+  do
+    TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$(basename "$DEP")"
+  done
+fi
 
 function target_shasum()
 (