proper target directory;
authorwenzelm
Mon, 07 Jun 2010 17:50:57 +0200
changeset 37460b7a55231065a
parent 37459 4f79bb1aaf50
child 37461 a2cde14de400
proper target directory;
Admin/makebundle
     1.1 --- a/Admin/makebundle	Mon Jun 07 17:50:40 2010 +0200
     1.2 +++ b/Admin/makebundle	Mon Jun 07 17:50:57 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz"
     1.5  [ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE"
     1.6  echo "heaps"
     1.7 -tar -C "$ISABELLE_HOME" -x -z -f "$HEAPS_ARCHIVE"
     1.8 +tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE"
     1.9  
    1.10  
    1.11  BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"