Admin/makedist
changeset 45109 20b3377b08d7
parent 45086 3933a0cbd049
child 45124 d78ec6c10fa1
equal deleted inserted replaced
45089:24ad77c3a147 45109:20b3377b08d7
     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-release"
     7 REPOS_NAME="isabelle"
     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