chmod u+rw on all files;
authorwenzelm
Sun, 22 Jul 2007 11:58:23 +0200
changeset 23895 89f8bfdbc269
parent 23894 1a4167d761ac
child 23896 26f92c405337
chmod u+rw on all files;
Admin/makedist
--- 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