Admin/makedist
changeset 10077 0261aede52ca
parent 10068 46db6fde4ee3
child 10087 4dc7edfb0b5f
equal deleted inserted replaced
10076:2683ff181047 10077:0261aede52ca
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # makedist -- make Isabelle distribution.
     5 # makedist -- make Isabelle source distribution.
     6 
     6 
     7 
     7 
     8 ## global settings
     8 ## global settings
     9 
     9 
    10 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL ZF"
    10 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL ZF"
   185 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML
   185 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML
   186 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   186 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   187 lynx -dump README.html >README
   187 lynx -dump README.html >README
   188 
   188 
   189 ( cd src; ../Admin/maketags; )
   189 ( cd src; ../Admin/maketags; )
       
   190 
       
   191 ( env BASH_PATH=/bin/bash PERL_PATH=/usr/bin/perl ./configure )
       
   192 
   190 rm -rf Admin
   193 rm -rf Admin
   191 
   194 
   192 
   195 
   193 # create archive
   196 # create archive
   194 
   197 
   200 
   203 
   201 rm -f Isabelle
   204 rm -f Isabelle
   202 ln -s "$DISTNAME" Isabelle
   205 ln -s "$DISTNAME" Isabelle
   203 
   206 
   204 chown -R "$LOGNAME" "$DISTNAME"
   207 chown -R "$LOGNAME" "$DISTNAME"
   205 chgrp -R isabelle "$DISTNAME"
       
   206 chmod -R u+w "$DISTNAME"
   208 chmod -R u+w "$DISTNAME"
   207 chmod -R g=o "$DISTNAME"
   209 chmod -R g=o "$DISTNAME"
       
   210 chgrp -R isabelle "$DISTNAME" Isabelle
   208 
   211 
   209 mkdir -p "pdf/$DISTNAME/doc"
   212 mkdir -p "pdf/$DISTNAME/doc"
   210 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   213 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   211 
   214 
   212 "$TAR" cf "$DISTNAME.tar" "$DISTNAME"
   215 echo "$DISTNAME.tar"
   213 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   216 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
       
   217 ( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   214 
   218 
   215 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   219 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   216 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   220 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   217 
   221 
   218 gzip "$DISTNAME.tar"
   222 echo "$DISTNAME.tar.gz" && gzip "$DISTNAME.tar"
   219 gzip "${DISTNAME}_pdf.tar"
   223 echo "${DISTNAME}_pdf.tar.gz" && gzip "${DISTNAME}_pdf.tar"
   220 
   224 
   221 
   225 
   222 # cleanup dist
   226 # cleanup dist
   223 
   227 
   224 mv "$DISTNAME" "${DISTNAME}-old"
   228 mv "$DISTNAME" "${DISTNAME}-old"