Admin/lib/Tools/makedist
changeset 61737 b91b1ebfc8a0
parent 57692 65dc798bb1fb
child 62114 a7cf464933f7
--- a/Admin/lib/Tools/makedist	Sun Nov 22 23:19:43 2015 +0100
+++ b/Admin/lib/Tools/makedist	Mon Nov 23 16:57:01 2015 +0100
@@ -207,8 +207,9 @@
 echo "$IDENT" >../ISABELLE_IDENT
 
 chown -R "$LOGNAME" "$DISTNAME"
+chmod -R g=o "$DISTNAME"
 chmod -R u+w "$DISTNAME"
-chmod -R g=o "$DISTNAME"
+find "$DISTNAME" -type f "(" -name '*.scala' -o -name '*.ML' -o -name '*.thy' ")" -print | xargs chmod -f u-w
 
 echo "$DISTBASE/$DISTNAME.tar.gz"
 tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"