# HG changeset patch
# User wenzelm
# Date 1185098303 -7200
# Node ID 89f8bfdbc269073b6983e4b0800d2e38e5f05f06
# Parent  1a4167d761ac251efd7b8e246219700b1f4a190d
chmod u+rw on all files;

diff -r 1a4167d761ac -r 89f8bfdbc269 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