Admin/makedist
changeset 41607 351aa5f7d130
parent 41560 20f33469cba7
child 41665 a23ca60625ef
equal deleted inserted replaced
41606:3d6f146e4cd0 41607:351aa5f7d130
     2 #
     2 #
     3 # makedist -- make Isabelle source distribution
     3 # makedist -- make Isabelle source distribution
     4 
     4 
     5 ## global settings
     5 ## global settings
     6 
     6 
     7 REPOS_NAME="isabelle"
     7 REPOS_NAME="isabelle-release"
     8 REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
     8 REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
     9 
     9 
    10 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
    10 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
    11 
    11 
    12 umask 022
    12 umask 022