--- 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" <<EOF
+<html>
+<head>
+<title>$DISTNAME Documentation</title>
+</head>
+<body>
+<h1>$DISTNAME Documentation</h1>
+$(cat "pdf/$DISTNAME/doc/index")
+</body>
+</html>
+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"