# HG changeset patch # User wenzelm # Date 1127494067 -7200 # Node ID 6527ba893bae769a4706127596905dd7bf261c02 # Parent caed4fb770d5c75b39e380011e94e8331f2a6436 removed doc/index.html from distribution (now produced by website); diff -r caed4fb770d5 -r 6527ba893bae Admin/makedist --- a/Admin/makedist Fri Sep 23 17:06:23 2005 +0200 +++ b/Admin/makedist Fri Sep 23 18:47:47 2005 +0200 @@ -219,20 +219,6 @@ mkdir -p "pdf/$DISTNAME/doc" mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" -#~ page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index" -#~ cat > "pdf/$DISTNAME/doc/index.html" < -#~ -#~ $DISTNAME Documentation -#~ -#~ -#~

$DISTNAME Documentation

-#~ $(cat "pdf/$DISTNAME/doc/index") -#~ -#~ -#~ EOF -#~ rm "pdf/$DISTNAME/doc/index" - echo "$DISTNAME.tar.gz" "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" gzip "$DISTNAME.tar" @@ -241,7 +227,7 @@ ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) gzip "${DISTNAME}_pdf.tar" -mv "pdf/$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc/index.html" "$DISTNAME/doc" +mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf @@ -254,7 +240,7 @@ "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ "$DISTNAME" mkdir "$DISTNAME/doc" -mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$DISTNAME/doc" +mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc" chgrp -R isabelle "$DISTNAME"