equal
deleted
inserted
replaced
11 umask 022 |
11 umask 022 |
12 |
12 |
13 |
13 |
14 ## diagnostics |
14 ## diagnostics |
15 |
15 |
16 PRG=$(basename "$0") |
16 PRG="$(basename "$0")" |
17 THIS=$(cd $(dirname "$0"); echo "$PWD") |
17 THIS="$(cd $(dirname "$0"); echo "$PWD")" |
18 |
18 |
19 function usage() |
19 function usage() |
20 { |
20 { |
21 cat <<EOF |
21 cat <<EOF |
22 |
22 |
129 |
129 |
130 echo "###" |
130 echo "###" |
131 echo "### Preparing distribution $DISTNAME" |
131 echo "### Preparing distribution $DISTNAME" |
132 echo "###" |
132 echo "###" |
133 |
133 |
134 find . -name .cvsignore -print | xargs rm -rf |
134 rm -f .hgignore |
135 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x |
135 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x |
136 find . -print | xargs chmod u+rw |
136 find . -print | xargs chmod -f u+rw |
137 |
137 |
138 ./Admin/build all || fail "Failed to build distribution" |
138 ./Admin/build all || fail "Failed to build distribution" |
139 rm -rf Admin |
139 rm -rf Admin |
140 |
140 |
141 MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
141 MOVE=$(find doc-src \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |