@documentdescription: Summary Text ¶When producing HTML output for a document, a ‘<meta>’ element
is written in the ‘<head>’ to give some idea of the
content of the document. By default, this description is the
title of the document, taken from the @settitle command
(see @settitle: Set the Document Title). To change this, use the
@documentdescription environment, as in:
@documentdescription descriptive text. @end documentdescription
This will produce the following output in the ‘<head>’ of the HTML:
<meta name=description content="descriptive text.">