-# documentation. (make-doc.sh needs to be run first, in order to
-# compile the DocBook sources into HTML.)
-
-# (Before sbcl-0.7.0, this functionality was part of
-# binary-distribution.sh.)
+# documentation. (cd doc/manual && make needs to be run first, in order to
+# compile the doc sources into HTML.)