# HG changeset patch
# User wenzelm
# Date 1239139550 -7200
# Node ID a3cfe0e27debfc278696e02e580977f25d514527
# Parent  59ce24e0abdad481234dd71f3738b78666694ddb
misc tuning and updates;

diff -r 59ce24e0abda -r a3cfe0e27deb Admin/makedist
--- a/Admin/makedist	Tue Apr 07 23:08:20 2009 +0200
+++ b/Admin/makedist	Tue Apr 07 23:25:50 2009 +0200
@@ -13,8 +13,8 @@
 
 ## diagnostics
 
-PRG=$(basename "$0")
-THIS=$(cd $(dirname "$0"); echo "$PWD")
+PRG="$(basename "$0")"
+THIS="$(cd $(dirname "$0"); echo "$PWD")"
 
 function usage()
 {
@@ -131,9 +131,9 @@
 echo "### Preparing distribution $DISTNAME"
 echo "###"
 
-find . -name .cvsignore -print | xargs rm -rf
+rm -f .hgignore
 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x
-find . -print | xargs chmod u+rw
+find . -print | xargs chmod -f u+rw
 
 ./Admin/build all || fail "Failed to build distribution"
 rm -rf Admin