more robust;
authorwenzelm
Sun, 12 Jan 2020 23:29:35 +0100
changeset 71371 1c4ec697bee5
parent 71370 b05aca9cee75
child 71372 85274743f789
more robust;
src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Jan 12 22:54:42 2020 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Jan 12 23:29:35 2020 +0100
@@ -325,7 +325,7 @@
 }
 
 target_shasum | cmp "$TARGET_SHASUM" 2>/dev/null
-if [ "$?" -ne 0 ]; then
+if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
   echo "### Building Isabelle/jEdit ..."
 
   [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \