Admin/makedist
changeset 29637 da018485b89d
parent 28942 043a42ba2a4d
child 30110 8cb4a8d6671f
equal deleted inserted replaced
29636:d01bada1df33 29637:da018485b89d
     1 #!/usr/bin/env bash
     1 #!/usr/bin/env bash
     2 #
     2 #
     3 # $Id$
       
     4 #
       
     5 # makedist -- make Isabelle source distribution
     3 # makedist -- make Isabelle source distribution
     6 
     4 
     7 ## global settings
     5 ## global settings
     8 
     6 
     9 REPOS="http://isabelle.in.tum.de/repos/isabelle"
     7 REPOS="https://isabelle.in.tum.de/repos/isabelle"
    10 
     8 
    11 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
     9 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
    12 
    10 
    13 umask 022
    11 umask 022
    14 
    12