equal
deleted
inserted
replaced
217 chgrp -R isabelle "$DISTNAME" Isabelle |
217 chgrp -R isabelle "$DISTNAME" Isabelle |
218 |
218 |
219 mkdir -p "pdf/$DISTNAME/doc" |
219 mkdir -p "pdf/$DISTNAME/doc" |
220 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
220 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" |
221 |
221 |
222 #~ page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index" |
|
223 #~ cat > "pdf/$DISTNAME/doc/index.html" <<EOF |
|
224 #~ <html> |
|
225 #~ <head> |
|
226 #~ <title>$DISTNAME Documentation</title> |
|
227 #~ </head> |
|
228 #~ <body> |
|
229 #~ <h1>$DISTNAME Documentation</h1> |
|
230 #~ $(cat "pdf/$DISTNAME/doc/index") |
|
231 #~ </body> |
|
232 #~ </html> |
|
233 #~ EOF |
|
234 #~ rm "pdf/$DISTNAME/doc/index" |
|
235 |
|
236 echo "$DISTNAME.tar.gz" |
222 echo "$DISTNAME.tar.gz" |
237 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
223 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" |
238 gzip "$DISTNAME.tar" |
224 gzip "$DISTNAME.tar" |
239 |
225 |
240 echo "${DISTNAME}_pdf.tar.gz" |
226 echo "${DISTNAME}_pdf.tar.gz" |
241 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
227 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) |
242 gzip "${DISTNAME}_pdf.tar" |
228 gzip "${DISTNAME}_pdf.tar" |
243 |
229 |
244 mv "pdf/$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc/index.html" "$DISTNAME/doc" |
230 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" |
245 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf |
231 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf |
246 |
232 |
247 |
233 |
248 # cleanup dist |
234 # cleanup dist |
249 |
235 |
252 |
238 |
253 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ |
239 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ |
254 "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ |
240 "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ |
255 "$DISTNAME" |
241 "$DISTNAME" |
256 mkdir "$DISTNAME/doc" |
242 mkdir "$DISTNAME/doc" |
257 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$DISTNAME/doc" |
243 mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc" |
258 |
244 |
259 chgrp -R isabelle "$DISTNAME" |
245 chgrp -R isabelle "$DISTNAME" |
260 |
246 |
261 rm -rf "${DISTNAME}-old" |
247 rm -rf "${DISTNAME}-old" |
262 |
248 |