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"