author | wenzelm |
Fri, 07 Mar 1997 16:40:30 +0100 | |
changeset 2776 | 7e99c2cbfb24 |
parent 2775 | 7a4989d685d6 |
child 2777 | 3396eb1fa01d |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Fri Mar 07 16:16:47 1997 +0100 +++ b/Admin/makedist Fri Mar 07 16:40:30 1997 +0100 @@ -142,9 +142,10 @@ cd $DISTBASE -chown -R $LOGNAME:isabelle $DISTNAME -chmod -R u+w $DISTNAME -chmod -R g-w $DISTNAME +#FIXME doesn't work!? +#chown -R $LOGNAME:isabelle $DISTNAME +#chmod -R u+w $DISTNAME +#chmod -R g-w $DISTNAME tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz