Admin/lib/Tools/makedist_bundle
changeset 67761 c07bc12d89f2
parent 66908 9b074f01a305
child 67994 11be98cefe92
--- 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"
       (