tuned;
authorwenzelm
Tue, 26 Sep 2000 18:09:38 +0200
changeset 10087 4dc7edfb0b5f
parent 10086 5245fa2ca8d3
child 10088 fe198ae54aa5
tuned;
Admin/makebin
Admin/makedist
--- a/Admin/makebin	Tue Sep 26 17:34:33 2000 +0200
+++ b/Admin/makebin	Tue Sep 26 18:09:38 2000 +0200
@@ -7,7 +7,7 @@
 
 ## global settings
 
-FAKE_BUILD=""
+FAKE_BUILD="true"
 DISTBASE=~/tmp/isadist
 TMP="/tmp/isabelle-makebin$$"
 
@@ -59,7 +59,7 @@
 mkdir "$TMP" || fail "Cannot create directory $TMP"
 
 cd "$TMP"
-tar -xzf "$ARCHIVE_FULL"
+"$TAR" xzf "$ARCHIVE_FULL"
 cd "$ISABELLE_NAME"
 
 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
@@ -92,7 +92,7 @@
 do
   "$TAR" cf "${IMG}_$PLATFORM.tar" "$ISABELLE_NAME/heaps/$COMPILER/$IMG"
   gzip "${IMG}_$PLATFORM.tar"
-  cp -f "${IMG}_$PLATFORM.tar.gz" "$DISTBASE"
+  cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
 done
 
 
--- a/Admin/makedist	Tue Sep 26 17:34:33 2000 +0200
+++ b/Admin/makedist	Tue Sep 26 18:09:38 2000 +0200
@@ -201,6 +201,8 @@
 
 cd "$DISTBASE"
 
+echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
+
 rm -f Isabelle
 ln -s "$DISTNAME" Isabelle