--- 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"