diff --git a/collects/scribblings/main/private/search.js b/collects/scribblings/main/private/search.js index 2ac4606b8f..df6bd70eee 100644 --- a/collects/scribblings/main/private/search.js +++ b/collects/scribblings/main/private/search.js @@ -643,7 +643,7 @@ function UncompactUrl(url) { function UncompactHtml(x) { if (typeof x == "string") { - return x; + return SanitizeHTML(x); } else if (!(x instanceof Array)) { return alert("Internal error in PLT docs"); } else if ((x.length == 2) && (typeof(x[0]) == "number")) {