Admin/makedist
changeset 4548 108b130efabf
parent 4542 e723ce456305
child 4549 aa02667fb3da
equal deleted inserted replaced
4547:3030c5b18580 4548:108b130efabf
   152 
   152 
   153 cd $DISTBASE
   153 cd $DISTBASE
   154 
   154 
   155 chown -R $LOGNAME:isabelle $DISTNAME
   155 chown -R $LOGNAME:isabelle $DISTNAME
   156 chmod -R u+w $DISTNAME
   156 chmod -R u+w $DISTNAME
   157 chmod -R g+w $DISTNAME
       
   158 
   157 
   159 if [ -n $(type -path gtar) ]; then
   158 if type -path gtar
       
   159 then
   160   gtar czf $DISTNAME.tar.gz $DISTNAME
   160   gtar czf $DISTNAME.tar.gz $DISTNAME
   161 else
   161 else
   162   tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz
   162   tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz
   163 fi
   163 fi
   164 
   164