diff -r 5e0b1ad1a447 -r 9a82e1c3d9da Admin/makedist --- a/Admin/makedist Wed Mar 03 11:27:10 1999 +0100 +++ b/Admin/makedist Thu Mar 04 14:23:51 1999 +0100 @@ -151,24 +151,12 @@ } >UNOFFICIAL fi +perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index1.html lib/html/index2.html perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html lynx -dump README.html >README -# prepare index.html - -perl -pi -e \ - "s/{ISABELLE}/$DISTNAME/g; \ - s/{PACKED_SIZE}/$PACKED_SIZE/g; \ - s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \ - s/{AUTHOR}/$LOGNAME/g; \ - s/{DATE}/$DATE/g;" \ - ../index.html \ - lib/html/index1.html \ - lib/html/index2.html - - # create archive cd $DISTBASE @@ -190,6 +178,17 @@ PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ] +# prepare dist index.html + +perl -pi -e \ + "s/{ISABELLE}/$DISTNAME/g; \ + s/{PACKED_SIZE}/$PACKED_SIZE/g; \ + s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \ + s/{AUTHOR}/$LOGNAME/g; \ + s/{DATE}/$DATE/g;" \ + index.html + + # final note echo