Make the footer at the end of a \verbatiminput stand out a little
more, to make it easier to tell apart from the verbatim content.
diff --git a/Doc/html/style.css b/Doc/html/style.css
index 5744630..4a9549f 100644
--- a/Doc/html/style.css
+++ b/Doc/html/style.css
@@ -89,6 +89,10 @@
monospace;
font-size: 90%; }
.verbatim { margin-left: 2em; }
+.verbatim .footer { padding: 0.05in;
+ font-size: 85%;
+ background-color: #99ccff;
+ margin-right: 0.5in; }
.grammar { background-color: #99ccff;
margin-right: 0.5in;