tuned;
authorwenzelm
Tue Sep 26 18:09:38 2000 +0200 (2000-09-26)
changeset 100874dc7edfb0b5f
parent 10086 5245fa2ca8d3
child 10088 fe198ae54aa5
tuned;
Admin/makebin
Admin/makedist
     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  
     2.1 --- a/Admin/makedist	Tue Sep 26 17:34:33 2000 +0200
     2.2 +++ b/Admin/makedist	Tue Sep 26 18:09:38 2000 +0200
     2.3 @@ -201,6 +201,8 @@
     2.4  
     2.5  cd "$DISTBASE"
     2.6  
     2.7 +echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
     2.8 +
     2.9  rm -f Isabelle
    2.10  ln -s "$DISTNAME" Isabelle
    2.11