diff --git a/webdoc/search.js b/webdoc/search.js index 05b35bddf..e09c15210 100644 --- a/webdoc/search.js +++ b/webdoc/search.js @@ -58,7 +58,8 @@ search_input.keyup (function (event) { $.each (data, function(key, val) { var item = val.name; - items.push('
  • ' + item + '
  • '); + var url = val.url.replace (/[<>]/g, function (c) { return c == '<' ? '{' : '}'; }); + items.push('
  • ' + item + '
  • '); }); var uls = $('