author | wenzelm |
Mon, 17 Mar 1997 10:39:57 +0100 | |
changeset 2794 | 2d259a41cd77 |
parent 2793 | b30c41754c86 |
child 2795 | d136fff43370 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Fri Mar 14 10:37:01 1997 +0100 +++ b/Admin/makedist Mon Mar 17 10:39:57 1997 +0100 @@ -142,10 +142,10 @@ cd $DISTBASE -#FIXME doesn't work!? -#chown -R $LOGNAME:isabelle $DISTNAME -#chmod -R u+w $DISTNAME -#chmod -R g-w $DISTNAME +#FIXME sometimes 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