tuned;
authorwenzelm
Tue, 24 Apr 2012 23:22:40 +0200
changeset 47739 19b914b7ac23
parent 47738 3531a8edcd48
child 47740 a8989fe9a3a5
tuned;
Admin/makedist
--- a/Admin/makedist	Tue Apr 24 23:03:59 2012 +0200
+++ b/Admin/makedist	Tue Apr 24 23:22:40 2012 +0200
@@ -142,7 +142,7 @@
 echo "###"
 
 rm -f .hgignore
-find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x
+find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
 find . -print | xargs chmod -f u+rw
 
 perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings