author | wenzelm |
Mon, 26 Sep 2005 15:56:28 +0200 | |
changeset 17651 | a6499b0c5a40 |
parent 17650 | 44b135d04cc4 |
child 17652 | b1ef33ebfa17 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Mon Sep 26 15:17:33 2005 +0200 +++ b/Admin/makedist Mon Sep 26 15:56:28 2005 +0200 @@ -217,7 +217,7 @@ chgrp -R isabelle "$DISTNAME" Isabelle mkdir -p "pdf/$DISTNAME/doc" -mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" +mv "$DISTNAME/doc/"*.pdf "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc" echo "$DISTNAME.tar.gz" "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"