equal
deleted
inserted
replaced
70 |
70 |
71 |
71 |
72 BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz" |
72 BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz" |
73 |
73 |
74 echo "$(basename "$BUNDLE_ARCHIVE")" |
74 echo "$(basename "$BUNDLE_ARCHIVE")" |
75 tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" Isabelle "$ISABELLE_NAME" |
75 tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" |
76 |
76 |
77 |
77 |
78 # clean up |
78 # clean up |
79 cd /tmp |
79 cd /tmp |
80 rm -rf "$TMP" |
80 rm -rf "$TMP" |