1.1 --- a/Admin/makebin	Tue Sep 26 17:34:33 2000 +0200
     1.2 +++ b/Admin/makebin	Tue Sep 26 18:09:38 2000 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  ## global settings
     1.6  
     1.7 -FAKE_BUILD=""
     1.8 +FAKE_BUILD="true"
     1.9  DISTBASE=~/tmp/isadist
    1.10  TMP="/tmp/isabelle-makebin$$"
    1.11  
    1.12 @@ -59,7 +59,7 @@
    1.13  mkdir "$TMP" || fail "Cannot create directory $TMP"
    1.14  
    1.15  cd "$TMP"
    1.16 -tar -xzf "$ARCHIVE_FULL"
    1.17 +"$TAR" xzf "$ARCHIVE_FULL"
    1.18  cd "$ISABELLE_NAME"
    1.19  
    1.20  ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
    1.21 @@ -92,7 +92,7 @@
    1.22  do
    1.23    "$TAR" cf "${IMG}_$PLATFORM.tar" "$ISABELLE_NAME/heaps/$COMPILER/$IMG"
    1.24    gzip "${IMG}_$PLATFORM.tar"
    1.25 -  cp -f "${IMG}_$PLATFORM.tar.gz" "$DISTBASE"
    1.26 +  cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
    1.27  done
    1.28  
    1.29