tuned;
authorwenzelm
Fri, 09 Jan 1998 14:28:20 +0100
changeset 4548 108b130efabf
parent 4547 3030c5b18580
child 4549 aa02667fb3da
tuned;
Admin/makedist
--- 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