# HG changeset patch
# User haftmann
# Date 1331733228 -3600
# Node ID f159e227703a987a9614aabb8c6f5f199d68ec10
# Parent  7eb9520eaf4b392a4d069e55d336e4b91020c576
corrected slip

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