Remove duplicate closing of </style>

Noted by Peter Eisentraut
This commit is contained in:
Magnus Hagander
2017-04-14 21:37:50 +02:00
parent d7957a214d
commit fb8ab1c4c5

View File

@ -19,7 +19,7 @@ if (newMonoSize != 1)
{ {
document.write('<style type="text/css" media="screen">' document.write('<style type="text/css" media="screen">'
+ '#docContainer tt, #docContainer pre, #docContainer code' + '#docContainer tt, #docContainer pre, #docContainer code'
+ '{font-size: ' + newMonoSize.toFixed(1) + 'em;}</style>\n' + '{font-size: ' + newMonoSize.toFixed(1) + 'em;}\n'
/* prevent embedded code tags from changing font size */ /* prevent embedded code tags from changing font size */
+ '#docContainer code code' + '#docContainer code code'
+ '{font-size: 1em;}</style>\n'); + '{font-size: 1em;}</style>\n');