diff -r 7eb9520eaf4b -r f159e227703a Admin/makedist
--- 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