--- a/Admin/makedist Tue Sep 05 18:53:21 2000 +0200
+++ b/Admin/makedist Tue Sep 05 18:53:42 2000 +0200
@@ -13,7 +13,6 @@
DISTPREFIX=~/tmp/isadist
umask 022
-newgrp isabelle
## diagnostics
@@ -80,7 +79,7 @@
DISTDATE=$(date "+%B %Y")
if [ "$VERSION" = "--" ]; then
- DISTNAME="Isabelle_$DATE_test"
+ DISTNAME="Isabelle_${DATE}_test"
DISTVERSION="$DISTNAME"
EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME"
UNOFFICIAL=""
@@ -218,6 +217,8 @@
mkdir "$DISTNAME/doc"
mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
+chgrp -R isabelle "$DISTNAME"
+
rm -rf "${DISTNAME}-old"