tuned;
authorwenzelm
Tue Sep 26 17:01:31 2000 +0200 (2000-09-26)
changeset 100770261aede52ca
parent 10076 2683ff181047
child 10078 8bb4b66cd6b5
tuned;
Admin/makedist
configure
     1.1 --- a/Admin/makedist	Tue Sep 26 16:42:24 2000 +0200
     1.2 +++ b/Admin/makedist	Tue Sep 26 17:01:31 2000 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  #
     1.5  # $Id$
     1.6  #
     1.7 -# makedist -- make Isabelle distribution.
     1.8 +# makedist -- make Isabelle source distribution.
     1.9  
    1.10  
    1.11  ## global settings
    1.12 @@ -187,6 +187,9 @@
    1.13  lynx -dump README.html >README
    1.14  
    1.15  ( cd src; ../Admin/maketags; )
    1.16 +
    1.17 +( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
    1.18 +
    1.19  rm -rf Admin
    1.20  
    1.21  
    1.22 @@ -202,21 +205,22 @@
    1.23  ln -s "$DISTNAME" Isabelle
    1.24  
    1.25  chown -R "$LOGNAME" "$DISTNAME"
    1.26 -chgrp -R isabelle "$DISTNAME"
    1.27  chmod -R u+w "$DISTNAME"
    1.28  chmod -R g=o "$DISTNAME"
    1.29 +chgrp -R isabelle "$DISTNAME" Isabelle
    1.30  
    1.31  mkdir -p "pdf/$DISTNAME/doc"
    1.32  mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
    1.33  
    1.34 -"$TAR" cf "$DISTNAME.tar" "$DISTNAME"
    1.35 -( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
    1.36 +echo "$DISTNAME.tar"
    1.37 +"$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
    1.38 +( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
    1.39  
    1.40  mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
    1.41  rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
    1.42  
    1.43 -gzip "$DISTNAME.tar"
    1.44 -gzip "${DISTNAME}_pdf.tar"
    1.45 +echo "$DISTNAME.tar.gz" && gzip "$DISTNAME.tar"
    1.46 +echo "${DISTNAME}_pdf.tar.gz" && gzip "${DISTNAME}_pdf.tar"
    1.47  
    1.48  
    1.49  # cleanup dist
     2.1 --- a/configure	Tue Sep 26 16:42:24 2000 +0200
     2.2 +++ b/configure	Tue Sep 26 17:01:31 2000 +0200
     2.3 @@ -8,11 +8,11 @@
     2.4  
     2.5  ## patch scripts
     2.6  
     2.7 -THIS=`dirname "$0"`
     2.8 +cd `dirname "$0"`
     2.9  
    2.10  if bash -c :
    2.11  then
    2.12 -  bash "$THIS/lib/scripts/patch-scripts.bash"
    2.13 +  bash lib/scripts/patch-scripts.bash
    2.14  else
    2.15    echo "FATAL ERROR: bash not found!"
    2.16    exit 2