author | wenzelm |
Fri, 09 Jan 1998 14:28:20 +0100 | |
changeset 4548 | 108b130efabf |
parent 4547 | 3030c5b18580 |
child 4549 | aa02667fb3da |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Fri Jan 09 14:03:39 1998 +0100 +++ b/Admin/makedist Fri Jan 09 14:28:20 1998 +0100 @@ -154,9 +154,9 @@ chown -R $LOGNAME:isabelle $DISTNAME chmod -R u+w $DISTNAME -chmod -R g+w $DISTNAME -if [ -n $(type -path gtar) ]; then +if type -path gtar +then gtar czf $DISTNAME.tar.gz $DISTNAME else tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz