src/Tools/jEdit/lib/Tools/jedit
changeset 71371 1c4ec697bee5
parent 71368 fd5cd1daf6a9
child 71372 85274743f789
--- 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" ] && \