--- a/Admin/makedist Thu Oct 12 08:10:23 2006 +0200
+++ b/Admin/makedist Thu Oct 12 08:25:04 2006 +0200
@@ -44,6 +44,7 @@
Checklist for official releases (before running this script):
+ * Symlink website to Admin/website
* Check Admin/website contents.
* Check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
* Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
@@ -136,10 +137,10 @@
for DOC in $(cat Contents)
do
- cd "$DOC"
+ pushd "$DOC" > /dev/null
make dvi || fail "DVI document for $DOC failed!"
{ [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!"
- cd ..
+ popd
done