# HG changeset patch
# User wenzelm
# Date 1520109564 -3600
# Node ID c07bc12d89f28bc6e52ebeb8a7d81c80c579e254
# Parent  553d9ad7d679688e821722e05696e1871d1943ee
more robust check -- do not rely on return code;

diff -r 553d9ad7d679 -r c07bc12d89f2 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Sat Mar 03 21:38:27 2018 +0100
+++ b/Admin/lib/Tools/makedist_bundle	Sat Mar 03 21:39:24 2018 +0100
@@ -398,8 +398,9 @@
   windows)
     (
       cd "$TMP"
-      rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.7z"
-      7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME" || exit 2
+      rm -f "$TMP/${ISABELLE_NAME}.7z"
+      7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME"
+      [ -f "$TMP/${ISABELLE_NAME}.7z" ] || exit 2
 
       echo "application for $PLATFORM_FAMILY"
       (