[m-rev.] trivial diff: improve appearance of HTML documentation

[Simon Taylor]

Estimated hours taken: 0.1
Branches: main, release

doc/texi2html:
	Use <h3> rather than <h2> for the version subtitles.
	The font Netscape uses for <h2> is too close to
	that used for <h1>.


Index: texi2html
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/texi2html,v
retrieving revision 1.4
diff -u -u -r1.4 texi2html
--- texi2html	3 Oct 2001 11:37:56 -0000	1.4
+++ texi2html	5 Oct 2001 07:52:10 -0000
@@ -1125,7 +1125,7 @@
 	foreach (split(/\n/, $value{'subtitle'})) {
 	    $_ = &substitute_style($_);
 	    &unprotect_texi;
-	    print FILE "<H2>$_</H2>\n";
+	    print FILE "<H3>$_</H3>\n";
 	}
     }
     if ($value{'author'}) {
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------