Admin/makedist
changeset 4548 108b130efabf
parent 4542 e723ce456305
child 4549 aa02667fb3da
--- 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