| changeset 46929 | f159e227703a |
| parent 46926 | 3978c15126e7 |
| child 46930 | 6d0a5549e2be |
--- a/Admin/makedist Wed Mar 14 12:39:26 2012 +0000 +++ b/Admin/makedist Wed Mar 14 14:53:48 2012 +0100 @@ -5,7 +5,7 @@ ## global settings REPOS_NAME="${REPOS_NAME:-isabelle}" -REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}" +REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}" DISTPREFIX="${DISTPREFIX:-~/tmp/isadist}" umask 022