Close #23: XH_highlightSearchWords() breaks Syntaxhighlighter

We employ an ugly fix for a real problem, which may not be our problem,
though.

syntaxhighlighter.min.js

@@ -22,6 +22,10 @@
         return;
     }
     document.addEventListener("DOMContentLoaded", function () {
+        Array.from(document.getElementsByClassName("brush:")).forEach(function (pre) {
+            // remove all HTML markup
+            pre.textContent = pre.textContent;
+        });
         var aboutDialog = SyntaxHighlighter.config.strings.aboutDialog;
         var brushes = JSON.parse(document.getElementsByName("syntaxhighlighter.brushes")[0].content);
         SyntaxHighlighter.autoloader(...brushes);