# HG changeset patch
# User wenzelm
# Date 884352500 -3600
# Node ID 108b130efabf18b6afac2afa1f614de83dd7982e
# Parent  3030c5b18580fd0a20df674b67d419f18dd0068c
tuned;

diff -r 3030c5b18580 -r 108b130efabf 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