Admin/makedist
changeset 10087 4dc7edfb0b5f
parent 10077 0261aede52ca
child 10096 6cbe69107c18
equal deleted inserted replaced
10086:5245fa2ca8d3 10087:4dc7edfb0b5f
   199 echo "### Creating archives ..."
   199 echo "### Creating archives ..."
   200 echo "###"
   200 echo "###"
   201 
   201 
   202 cd "$DISTBASE"
   202 cd "$DISTBASE"
   203 
   203 
       
   204 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
       
   205 
   204 rm -f Isabelle
   206 rm -f Isabelle
   205 ln -s "$DISTNAME" Isabelle
   207 ln -s "$DISTNAME" Isabelle
   206 
   208 
   207 chown -R "$LOGNAME" "$DISTNAME"
   209 chown -R "$LOGNAME" "$DISTNAME"
   208 chmod -R u+w "$DISTNAME"
   210 chmod -R u+w "$DISTNAME"