Admin/makedist
changeset 33909 24a9d433eb7f
parent 33899 07ab63b320dd
child 33910 bae240a8bfe9
     1.1 --- a/Admin/makedist	Fri Nov 27 00:59:01 2009 +0100
     1.2 +++ b/Admin/makedist	Fri Nov 27 22:38:22 2009 +0100
     1.3 @@ -4,7 +4,8 @@
     1.4  
     1.5  ## global settings
     1.6  
     1.7 -REPOS="http://isabelle.in.tum.de/repos/isabelle-release"
     1.8 +REPOS_NAME="isabelle-release"
     1.9 +REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
    1.10  
    1.11  DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
    1.12  
    1.13 @@ -92,12 +93,12 @@
    1.14  { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
    1.15    fail "Failed to retrieve $VERSION"
    1.16  
    1.17 -IDENT=$(echo * | sed 's/isabelle-//')
    1.18 +IDENT=$(echo * | sed 's/${REPOS_NAME}-//')
    1.19  
    1.20 -rm -f "isabelle-$IDENT/.hg_archival.txt"
    1.21 -rm -f "isabelle-$IDENT/.hgtags"
    1.22 -rm -f "isabelle-$IDENT/.hgignore"
    1.23 -rm -f "isabelle-$IDENT/README_REPOSITORY"
    1.24 +rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
    1.25 +rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
    1.26 +rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
    1.27 +rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
    1.28  
    1.29  
    1.30  # dist name
    1.31 @@ -118,7 +119,7 @@
    1.32  [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
    1.33  
    1.34  cd "$DISTBASE"
    1.35 -mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
    1.36 +mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
    1.37  purge_tmp
    1.38  
    1.39  cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"