--- 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" <<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"
@@ -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"