# HG changeset patch
# User wenzelm
# Date 1620678722 -7200
# Node ID 8b3e672df28c9c42851c508de73bc31376086f78
# Parent  ff716ecb08053b1a9fd6045eb1c45afd333f7e44
proper build for fresh target directory (amending d9823224fcfe);

diff -r ff716ecb0805 -r 8b3e672df28c 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()
 (