# HG changeset patch
# User wenzelm
# Date 969980491 -7200
# Node ID 0261aede52ca1271814bb71c077f7d174673ddff
# Parent  2683ff1810477626c0119da707456e06734d1a0b
tuned;

diff -r 2683ff181047 -r 0261aede52ca Admin/makedist
--- a/Admin/makedist	Tue Sep 26 16:42:24 2000 +0200
+++ b/Admin/makedist	Tue Sep 26 17:01:31 2000 +0200
@@ -2,7 +2,7 @@
 #
 # $Id$
 #
-# makedist -- make Isabelle distribution.
+# makedist -- make Isabelle source distribution.
 
 
 ## global settings
@@ -187,6 +187,9 @@
 lynx -dump README.html >README
 
 ( cd src; ../Admin/maketags; )
+
+( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
+
 rm -rf Admin
 
 
@@ -202,21 +205,22 @@
 ln -s "$DISTNAME" Isabelle
 
 chown -R "$LOGNAME" "$DISTNAME"
-chgrp -R isabelle "$DISTNAME"
 chmod -R u+w "$DISTNAME"
 chmod -R g=o "$DISTNAME"
+chgrp -R isabelle "$DISTNAME" Isabelle
 
 mkdir -p "pdf/$DISTNAME/doc"
 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
 
-"$TAR" cf "$DISTNAME.tar" "$DISTNAME"
-( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
+echo "$DISTNAME.tar"
+"$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
+( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
 
 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
 
-gzip "$DISTNAME.tar"
-gzip "${DISTNAME}_pdf.tar"
+echo "$DISTNAME.tar.gz" && gzip "$DISTNAME.tar"
+echo "${DISTNAME}_pdf.tar.gz" && gzip "${DISTNAME}_pdf.tar"
 
 
 # cleanup dist
diff -r 2683ff181047 -r 0261aede52ca configure
--- a/configure	Tue Sep 26 16:42:24 2000 +0200
+++ b/configure	Tue Sep 26 17:01:31 2000 +0200
@@ -8,11 +8,11 @@
 
 ## patch scripts
 
-THIS=`dirname "$0"`
+cd `dirname "$0"`
 
 if bash -c :
 then
-  bash "$THIS/lib/scripts/patch-scripts.bash"
+  bash lib/scripts/patch-scripts.bash
 else
   echo "FATAL ERROR: bash not found!"
   exit 2