author | wenzelm |
Sun, 22 Jul 2007 11:58:23 +0200 | |
changeset 23895 | 89f8bfdbc269 |
parent 23894 | 1a4167d761ac |
child 23896 | 26f92c405337 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Sat Jul 21 23:25:00 2007 +0200 +++ b/Admin/makedist Sun Jul 22 11:58:23 2007 +0200 @@ -124,6 +124,7 @@ $FIND . -name CVS -print | xargs rm -rf $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 # build docs