equal
deleted
inserted
replaced
11 |
11 |
12 export CVSROOT=/usr/proj/isabelle-repository/archive |
12 export CVSROOT=/usr/proj/isabelle-repository/archive |
13 DISTPREFIX=~/tmp/isadist |
13 DISTPREFIX=~/tmp/isadist |
14 |
14 |
15 umask 022 |
15 umask 022 |
|
16 |
|
17 TAR=tar |
|
18 type -path gtar >/dev/null && TAR=gtar |
|
19 |
|
20 FIND=find |
|
21 type -path gfind >/dev/null && FIND=gfind |
16 |
22 |
17 |
23 |
18 ## diagnostics |
24 ## diagnostics |
19 |
25 |
20 PRG=$(basename "$0") |
26 PRG=$(basename "$0") |
108 echo "###" |
114 echo "###" |
109 |
115 |
110 cd "$DISTBASE" |
116 cd "$DISTBASE" |
111 |
117 |
112 $EXPORT |
118 $EXPORT |
113 find . -name CVS -print | xargs rm -rf |
119 $FIND . -name CVS -print | xargs rm -rf |
114 find . "(" -type d -a -empty ")" -print | xargs rm -f |
120 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf |
115 find . "(" -type d -a -empty ")" -print | xargs rm -f |
121 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf |
116 find . "(" -type d -a -empty ")" -print | xargs rm -f |
122 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf |
117 |
123 |
118 |
124 |
119 # build docs |
125 # build docs |
120 |
126 |
121 echo "###" |
127 echo "###" |
126 PDFLATEX=$(type -path pdflatex) |
132 PDFLATEX=$(type -path pdflatex) |
127 |
133 |
128 for DOC in $(cat Contents) |
134 for DOC in $(cat Contents) |
129 do |
135 do |
130 cd "$DOC" |
136 cd "$DOC" |
131 make dvi |
137 #FIXME make dvi |
132 [ -n "$PDFLATEX" ] && make clean pdf |
138 #FIXME [ -n "$PDFLATEX" ] && make clean pdf |
133 cd .. |
139 cd .. |
134 done |
140 done |
135 |
141 |
136 |
142 |
137 # make WWW pages |
|
138 |
|
139 #FIXME |
|
140 #export DISTNAME |
|
141 #( cd "$DISTBASE/$DISTNAME/Admin/page"; make clean; make dist; cd dist; cp * "$DISTBASE"; ) |
|
142 |
|
143 |
|
144 # prepare dist dir for release |
143 # prepare dist dir for release |
145 |
144 |
|
145 echo "###" |
|
146 echo "### Preparing distribution ..." |
|
147 echo "###" |
|
148 |
146 cd "$DISTBASE/$DISTNAME" |
149 cd "$DISTBASE/$DISTNAME" |
147 |
150 |
148 MOVE=$(find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
151 cp -R Admin/page ../page |
|
152 cp Distribution/Doc/Contents ../page/Contents |
|
153 cp Distribution/lib/logo/isabelle.gif ../page/main-content |
|
154 cp Distribution/lib/logo/isabelle.gif ../page/dist-content |
|
155 echo "$DISTNAME" > ../page/DISTNAME |
|
156 |
|
157 MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
149 mv -f $MOVE Distribution/doc |
158 mv -f $MOVE Distribution/doc |
150 rm Distribution/doc/Isa-logics.eps |
159 rm Distribution/doc/Isa-logics.eps |
151 rm -rf Doc Tools |
160 rm -rf Doc Tools |
152 |
161 |
153 mkdir src contrib |
162 mkdir src contrib |
192 chown -R "$LOGNAME" "$DISTNAME" |
201 chown -R "$LOGNAME" "$DISTNAME" |
193 chgrp -R isabelle "$DISTNAME" |
202 chgrp -R isabelle "$DISTNAME" |
194 chmod -R u+w "$DISTNAME" |
203 chmod -R u+w "$DISTNAME" |
195 chmod -R g=o "$DISTNAME" |
204 chmod -R g=o "$DISTNAME" |
196 |
205 |
197 TAR=tar |
|
198 type -path gtar >/dev/null && TAR=gtar |
|
199 |
|
200 mkdir -p "pdf/$DISTNAME/doc" |
206 mkdir -p "pdf/$DISTNAME/doc" |
201 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
207 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
202 |
208 |
203 "$TAR" cf "$DISTNAME.tar" "$DISTNAME" |
209 "$TAR" cf "$DISTNAME.tar" "$DISTNAME" |
204 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
210 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
213 # cleanup dist |
219 # cleanup dist |
214 |
220 |
215 mv "$DISTNAME" "${DISTNAME}-old" |
221 mv "$DISTNAME" "${DISTNAME}-old" |
216 mkdir "$DISTNAME" |
222 mkdir "$DISTNAME" |
217 |
223 |
218 mv "${DISTNAME}-old/lib/logo/isabelle.gif" . |
|
219 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME" |
224 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME" |
220 mkdir "$DISTNAME/doc" |
225 mkdir "$DISTNAME/doc" |
221 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
226 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
222 |
227 |
223 chgrp -R isabelle "$DISTNAME" |
228 chgrp -R isabelle "$DISTNAME" |
224 |
229 |
225 rm -rf "${DISTNAME}-old" |
230 rm -rf "${DISTNAME}-old" |
226 |
231 |
227 |
232 |
228 # prepare web pages |
|
229 |
|
230 #FIXME |
|
231 #$THIS/filesizes -norpm |
|
232 |
|
233 |
|
234 # final note |
233 # final note |
235 |
234 |
236 echo "###" |
235 echo "###" |
237 echo "### Finished. You will find the distribution in $DISTBASE." |
236 echo "### Finished." |
238 echo "###" |
237 echo "###" |