1.1 --- a/Admin/makedist	Tue Apr 07 23:08:20 2009 +0200
     1.2 +++ b/Admin/makedist	Tue Apr 07 23:25:50 2009 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4  
     1.5  ## diagnostics
     1.6  
     1.7 -PRG=$(basename "$0")
     1.8 -THIS=$(cd $(dirname "$0"); echo "$PWD")
     1.9 +PRG="$(basename "$0")"
    1.10 +THIS="$(cd $(dirname "$0"); echo "$PWD")"
    1.11  
    1.12  function usage()
    1.13  {
    1.14 @@ -131,9 +131,9 @@
    1.15  echo "### Preparing distribution $DISTNAME"
    1.16  echo "###"
    1.17  
    1.18 -find . -name .cvsignore -print | xargs rm -rf
    1.19 +rm -f .hgignore
    1.20  find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x
    1.21 -find . -print | xargs chmod u+rw
    1.22 +find . -print | xargs chmod -f u+rw
    1.23  
    1.24  ./Admin/build all || fail "Failed to build distribution"
    1.25  rm -rf Admin