diff --git a/doc/sh_main.js b/doc/sh_main.js index 1d59dc7dcf..27905696c8 100644 --- a/doc/sh_main.js +++ b/doc/sh_main.js @@ -547,6 +547,7 @@ function highlight(prefix, suffix, tag) { function sh_highlightDocument(prefix, suffix) { + highlight(prefix, suffix, 'tt'); highlight(prefix, suffix, 'code'); highlight(prefix, suffix, 'pre'); }