-# the various binary files, and make-doc.sh, or possibly some other
-# DocBook-to-HTML converter, should also be run to create the
-# HTML version of the documentation.)
+# the various binary files, and make-doc.sh should also be run to
+# create the HTML version of the documentation.)