equal
deleted
inserted
replaced
140 echo "###" |
140 echo "###" |
141 echo "### Preparing distribution $DISTNAME" |
141 echo "### Preparing distribution $DISTNAME" |
142 echo "###" |
142 echo "###" |
143 |
143 |
144 rm -f .hgignore |
144 rm -f .hgignore |
145 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x |
145 find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x |
146 find . -print | xargs chmod -f u+rw |
146 find . -print | xargs chmod -f u+rw |
147 |
147 |
148 perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings |
148 perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings |
149 |
149 |
150 ./Admin/build all || fail "Failed to build distribution" |
150 ./Admin/build all || fail "Failed to build distribution" |