# HG changeset patch # User haftmann # Date 1119334563 -7200 # Node ID 5e5945ae284cfc1e2bafbf8d59987dedb051f8ae # Parent ee552def87219c701f6f2d62e0c5d77e87652769 removed mkcontent from makedist diff -r ee552def8721 -r 5e5945ae284c Admin/makedist --- a/Admin/makedist Tue Jun 21 00:45:56 2005 +0200 +++ b/Admin/makedist Tue Jun 21 08:16:03 2005 +0200 @@ -236,19 +236,19 @@ 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" +#~ 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"