Admin/makebundle
changeset 41555 178fdd4cca46
parent 37357 b7a55231065a
child 41611 f23ce44fbaec
     1.1 --- a/Admin/makebundle	Fri Jan 14 17:20:36 2011 +0100
     1.2 +++ b/Admin/makebundle	Fri Jan 14 18:23:39 2011 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4  BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
     1.5  
     1.6  echo "$(basename "$BUNDLE_ARCHIVE")"
     1.7 -tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" Isabelle "$ISABELLE_NAME"
     1.8 +tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME"
     1.9  
    1.10  
    1.11  # clean up