From fb8ab1c4c5f254a7a9d3665a0cc40ad813192841 Mon Sep 17 00:00:00 2001
From: Magnus Hagander <magnus@hagander.net>
Date: Fri, 14 Apr 2017 21:37:50 +0200
Subject: [PATCH] Remove duplicate closing of </style>

Noted by Peter Eisentraut
---
 media/js/monospacefix.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/media/js/monospacefix.js b/media/js/monospacefix.js
index 42ce9139..e7f117e3 100644
--- a/media/js/monospacefix.js
+++ b/media/js/monospacefix.js
@@ -19,7 +19,7 @@ if (newMonoSize != 1)
 {
         document.write('<style type="text/css" media="screen">'
 					+ '#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 */
 					+ '#docContainer code code'
 					+ '{font-size: 1em;}</style>\n');