author | paulson |
Wed, 14 Mar 2012 12:39:26 +0000 | |
changeset 46928 | 7eb9520eaf4b |
parent 46926 | 3978c15126e7 (diff) |
parent 46927 | faf4a0b02b71 (current diff) |
child 46929 | f159e227703a |
--- a/Admin/makedist Wed Mar 14 12:39:04 2012 +0000 +++ b/Admin/makedist Wed Mar 14 12:39:26 2012 +0000 @@ -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