merged
authorpaulson
Wed, 14 Mar 2012 12:39:26 +0000
changeset 46928 7eb9520eaf4b
parent 46926 3978c15126e7 (diff)
parent 46927 faf4a0b02b71 (current diff)
child 46929 f159e227703a
merged
--- a/Admin/makedist	Wed Mar 14 12:39:04 2012 +0000
+++ b/Admin/makedist	Wed Mar 14 12:39:26 2012 +0000
@@ -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