dbhtml_linenumbering.width — Specifies width for line numbers in verbatims
<?dbhtml linenumbering.width="width"?>Use the <?dbhtml linenumbering.width?> PI as a child
of a “verbatim” element – programlisting,
screen, synopsis — to specify
the width set aside for line numbers.