diff -r c04bbfe71cef -r 0c1296049b47 Admin/makedist
--- 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