Admin/makedist
changeset 4181 fcc8b47e4c49
parent 4180 2f0df5b390e8
child 4411 345d2c67a5b5
equal deleted inserted replaced
4180:2f0df5b390e8 4181:fcc8b47e4c49
   150 
   150 
   151 # create archive
   151 # create archive
   152 
   152 
   153 cd $DISTBASE
   153 cd $DISTBASE
   154 
   154 
   155 #FIXME sometimes doesn't work!?
       
   156 chown -R $LOGNAME:isabelle $DISTNAME
   155 chown -R $LOGNAME:isabelle $DISTNAME
   157 chmod -R u+w $DISTNAME
   156 chmod -R u+w $DISTNAME
   158 chmod -R g+w $DISTNAME
   157 chmod -R g+w $DISTNAME
   159 
   158 
   160 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz
   159 tar cf - $DISTNAME | gzip >$DISTNAME.tar.gz