# HG changeset patch
# User wenzelm
# Date 1259357902 -3600
# Node ID 24a9d433eb7f4d67812d399bbef7d74e13588fa7
# Parent  7c473c4d42f4ca43dc4d8db8a833076cd755ca1f
more abstract handling of repository name;

diff -r 7c473c4d42f4 -r 24a9d433eb7f Admin/makedist
--- a/Admin/makedist	Fri Nov 27 00:59:01 2009 +0100
+++ b/Admin/makedist	Fri Nov 27 22:38:22 2009 +0100
@@ -4,7 +4,8 @@
 
 ## global settings
 
-REPOS="http://isabelle.in.tum.de/repos/isabelle-release"
+REPOS_NAME="isabelle-release"
+REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
 
 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
 
@@ -92,12 +93,12 @@
 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
   fail "Failed to retrieve $VERSION"
 
-IDENT=$(echo * | sed 's/isabelle-//')
+IDENT=$(echo * | sed 's/${REPOS_NAME}-//')
 
-rm -f "isabelle-$IDENT/.hg_archival.txt"
-rm -f "isabelle-$IDENT/.hgtags"
-rm -f "isabelle-$IDENT/.hgignore"
-rm -f "isabelle-$IDENT/README_REPOSITORY"
+rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
+rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
+rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
+rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
 
 
 # dist name
@@ -118,7 +119,7 @@
 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
 
 cd "$DISTBASE"
-mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
+mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
 purge_tmp
 
 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"