| changeset 30287 | 39b931e00ba9 |
| parent 30140 | 45cf6c04846e |
| child 30858 | 2048e99f4e3e |
--- a/Admin/makedist Thu Mar 05 17:35:37 2009 +0100 +++ b/Admin/makedist Thu Mar 05 18:19:20 2009 +0100 @@ -144,7 +144,7 @@ echo "###" find . -name .cvsignore -print | xargs rm -rf -find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x +find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x find . -print | xargs chmod u+rw ./Admin/build all || fail "Failed to build distribution"