# HG changeset patch
# User haftmann
# Date 1331724042 -3600
# Node ID 3978c15126e7ceccf540fae0553e78a2c02b9fab
# Parent  c2ca2c3d23a689b3d2065068cae9c93dd071b277
allow modification of REPOS_NAME and REPOS from outside

diff -r c2ca2c3d23a6 -r 3978c15126e7 Admin/makedist
--- a/Admin/makedist	Wed Mar 14 00:34:56 2012 +0100
+++ b/Admin/makedist	Wed Mar 14 12:20:42 2012 +0100
@@ -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