# HG changeset patch
# User wenzelm
# Date 1335302560 -7200
# Node ID 19b914b7ac2398ca8d1c99cb37329980d437f400
# Parent  3531a8edcd4893aa199df2bd75cf884121772e2a
tuned;

diff -r 3531a8edcd48 -r 19b914b7ac23 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