From eb7fa6f066d2109e856cf00050ef1e05598844c6 Mon Sep 17 00:00:00 2001
From: Danny Yoo <dyoo@hashcollision.org>
Date: Mon, 25 Mar 2013 12:35:26 -0600
Subject: [PATCH] Sanitize the output from HTML escape characters.

Noted by ozzloy on IRC.  The search page appears to fail when
searching for the term 'string<?'; in truth, the search succeeds, but
the search link-printing code doesn't escape the '<?' part of the
identifier.
---
 collects/scribblings/main/private/search.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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")) {