removed mkcontent from makedist
authorhaftmann
Tue Jun 21 08:16:03 2005 +0200 (2005-06-21)
changeset 165085e5945ae284c
parent 16507 ee552def8721
child 16509 20f4c6a950f7
removed mkcontent from makedist
Admin/makedist
     1.1 --- a/Admin/makedist	Tue Jun 21 00:45:56 2005 +0200
     1.2 +++ b/Admin/makedist	Tue Jun 21 08:16:03 2005 +0200
     1.3 @@ -236,19 +236,19 @@
     1.4  mkdir -p "pdf/$DISTNAME/doc"
     1.5  mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
     1.6  
     1.7 -page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index"
     1.8 -cat > "pdf/$DISTNAME/doc/index.html" <<EOF
     1.9 -<html>
    1.10 -<head>
    1.11 -<title>$DISTNAME Documentation</title>
    1.12 -</head>
    1.13 -<body>
    1.14 -<h1>$DISTNAME Documentation</h1>
    1.15 -$(cat "pdf/$DISTNAME/doc/index")
    1.16 -</body>
    1.17 -</html>
    1.18 -EOF
    1.19 -rm "pdf/$DISTNAME/doc/index"
    1.20 +#~ page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index"
    1.21 +#~ cat > "pdf/$DISTNAME/doc/index.html" <<EOF
    1.22 +#~ <html>
    1.23 +#~ <head>
    1.24 +#~ <title>$DISTNAME Documentation</title>
    1.25 +#~ </head>
    1.26 +#~ <body>
    1.27 +#~ <h1>$DISTNAME Documentation</h1>
    1.28 +#~ $(cat "pdf/$DISTNAME/doc/index")
    1.29 +#~ </body>
    1.30 +#~ </html>
    1.31 +#~ EOF
    1.32 +#~ rm "pdf/$DISTNAME/doc/index"
    1.33  
    1.34  echo "$DISTNAME.tar.gz"
    1.35  "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"