1.1 --- a/Admin/makedist_mercurial	Tue Aug 26 12:07:06 2008 +0200
     1.2 +++ b/Admin/makedist_mercurial	Tue Aug 26 12:17:58 2008 +0200
     1.3 @@ -94,10 +94,10 @@
     1.4  { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
     1.5    fail "Failed to retrieve $VERSION"
     1.6  
     1.7 -IDENT=$(echo * | sed 's/Isabelle-repository-//')
     1.8 +IDENT=$(echo * | sed 's/isabelle-//')
     1.9  
    1.10 -rm -f "Isabelle-repository-$IDENT/.hg_archival.txt"
    1.11 -rm -f "Isabelle-repository-$IDENT/.hgtags"
    1.12 +rm -f "isabelle-$IDENT/.hg_archival.txt"
    1.13 +rm -f "isabelle-$IDENT/.hgtags"
    1.14  
    1.15  
    1.16  # dist name
    1.17 @@ -119,7 +119,7 @@
    1.18  [ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
    1.19  
    1.20  cd "$DISTBASE"
    1.21 -mv "$DISTPREFIX/$TMP/Isabelle-repository-$IDENT" "$DISTNAME"
    1.22 +mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
    1.23  purge_tmp
    1.24  
    1.25  cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"