| changeset 46926 | 3978c15126e7 |
| parent 45124 | d78ec6c10fa1 |
| child 46929 | f159e227703a |
--- a/Admin/makedist Wed Mar 14 00:34:56 2012 +0100 +++ b/Admin/makedist Wed Mar 14 12:20:42 2012 +0100 @@ -4,10 +4,9 @@ ## global settings -REPOS_NAME="isabelle" -REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}" - -DISTPREFIX=${DISTPREFIX:-~/tmp/isadist} +REPOS_NAME="${REPOS_NAME:-isabelle}" +REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}" +DISTPREFIX="${DISTPREFIX:-~/tmp/isadist}" umask 022