# HG changeset patch
# User wenzelm
# Date 1219745878 -7200
# Node ID 95bd956c476c6801922cb48efa096b52011e06e1
# Parent  4642317e0deb78ace43cb6d9e2cf67f31e04d49b
renamed Isabelle-repository to isabelle;

diff -r 4642317e0deb -r 95bd956c476c Admin/makedist_mercurial
--- a/Admin/makedist_mercurial	Tue Aug 26 12:07:06 2008 +0200
+++ b/Admin/makedist_mercurial	Tue Aug 26 12:17:58 2008 +0200
@@ -94,10 +94,10 @@
 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
   fail "Failed to retrieve $VERSION"
 
-IDENT=$(echo * | sed 's/Isabelle-repository-//')
+IDENT=$(echo * | sed 's/isabelle-//')
 
-rm -f "Isabelle-repository-$IDENT/.hg_archival.txt"
-rm -f "Isabelle-repository-$IDENT/.hgtags"
+rm -f "isabelle-$IDENT/.hg_archival.txt"
+rm -f "isabelle-$IDENT/.hgtags"
 
 
 # dist name
@@ -119,7 +119,7 @@
 [ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
 
 cd "$DISTBASE"
-mv "$DISTPREFIX/$TMP/Isabelle-repository-$IDENT" "$DISTNAME"
+mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
 purge_tmp
 
 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"