Admin/makedist
changeset 47739 19b914b7ac23
parent 47011 1d8601c642cc
child 47862 d9a09f965dab
--- 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