# HG changeset patch
# User wenzelm
# Date 969984578 -7200
# Node ID 4dc7edfb0b5fb249ac17a259260113dee29e8640
# Parent  5245fa2ca8d37814a491e23191608fdaaa669db8
tuned;

diff -r 5245fa2ca8d3 -r 4dc7edfb0b5f Admin/makebin
--- 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
 
 
diff -r 5245fa2ca8d3 -r 4dc7edfb0b5f Admin/makedist
--- 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