corrected slip
authorhaftmann
Wed, 14 Mar 2012 14:53:48 +0100
changeset 46929 f159e227703a
parent 46928 7eb9520eaf4b
child 46930 6d0a5549e2be
child 46935 38ecb2dc3636
corrected slip
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