| 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