# HG changeset patch
# User wenzelm
# Date 1216322612 -7200
# Node ID 70973f73f09d8e939b2bd68c5c0ed3ecce0f5029
# Parent  ee452b218407c58e6fb178bfa3c7bc4a3741ae3c
proper purge_tmp;
remove .cvsignore files;

diff -r ee452b218407 -r 70973f73f09d Admin/makedist_mercurial
--- a/Admin/makedist_mercurial	Thu Jul 17 21:23:08 2008 +0200
+++ b/Admin/makedist_mercurial	Thu Jul 17 21:23:32 2008 +0200
@@ -9,7 +9,6 @@
 REPOS="http://isabelle.in.tum.de/isabelle-bin/mercurial.cgi"
 
 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
-TMP="tmp-$USER$$"
 
 umask 022
 
@@ -84,6 +83,12 @@
 
 ## main
 
+# tmp
+
+TMP="tmp-$USER$$"
+function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
+
+
 # retrieve archive and resolve version identifier
 
 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
@@ -117,13 +122,13 @@
 fi
 
 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
-mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"
-[ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!"
-[ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"
+mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
+[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
+[ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
 
 cd "$DISTBASE"
 mv "$DISTPREFIX/$TMP/Isabelle-repository-$IDENT" "$DISTNAME"
-rm -rf "$DISTPREFIX/$TMP"
+purge_tmp
 
 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
 
@@ -147,6 +152,7 @@
 echo "### Preparing distribution $DISTNAME"
 echo "###"
 
+find . -name .cvsignore -print | xargs rm -rf
 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
 find . -print | xargs chmod u+rw