# HG changeset patch # User wenzelm # Date 979846539 -3600 # Node ID e040e8627bbb7861fda39bfdce23810b4b1628eb # Parent 33e290a704457e9f33cec1a8beec48b40b8b1430 generate index.html for pdf docs; diff -r 33e290a70445 -r e040e8627bbb Admin/makedist --- a/Admin/makedist Thu Jan 18 20:23:51 2001 +0100 +++ b/Admin/makedist Thu Jan 18 20:35:39 2001 +0100 @@ -222,6 +222,20 @@ 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" @@ -230,7 +244,7 @@ ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) gzip "${DISTNAME}_pdf.tar" -mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" +mv "pdf/$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc/index.html" "$DISTNAME/doc" rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf @@ -241,7 +255,7 @@ mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" "$DISTNAME" mkdir "$DISTNAME/doc" -mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc" +mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$DISTNAME/doc" chgrp -R isabelle "$DISTNAME"