# HG changeset patch
# User haftmann
# Date 1331735047 -3600
# Node ID 6d0a5549e2be7fa9fe5abd686898181a973b9493
# Parent  f159e227703a987a9614aabb8c6f5f199d68ec10
support for non-HTTP repository locations (important for mira); quasi-hardwired repository name

diff -r f159e227703a -r 6d0a5549e2be Admin/makedist
--- a/Admin/makedist	Wed Mar 14 14:53:48 2012 +0100
+++ b/Admin/makedist	Wed Mar 14 15:24:07 2012 +0100
@@ -4,7 +4,7 @@
 
 ## global settings
 
-REPOS_NAME="${REPOS_NAME:-isabelle}"
+REPOS_NAME="isabelle"
 REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
 DISTPREFIX="${DISTPREFIX:-~/tmp/isadist}"
 
@@ -94,8 +94,14 @@
 echo "### Retrieving Mercurial repository $VERSION"
 echo "###"
 
-{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
-  fail "Failed to retrieve $VERSION"
+if expr match "$REPOS" "https\?://" > /dev/null
+then
+  { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
+    fail "Failed to retrieve $VERSION"
+else
+  { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
+    fail "Failed to retrieve $VERSION"
+fi
 
 IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
 
@@ -224,5 +230,4 @@
 
 rm -rf "${DISTNAME}-old"
 
-
 echo "DONE"