From d1525edf62a1db2ade3c64dd17eb81bff87a4112 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Sun, 11 May 2014 07:45:25 -0600 Subject: [PATCH] Scribble search, etc.: fix URL decoding Use Javascript's decodeURIComponent() instead of unescape(). This repair makes searching for Unicode characters work from DrRacket (e.g., via F1). --- pkgs/scribble-pkgs/scribble-lib/scribble/scribble-common.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pkgs/scribble-pkgs/scribble-lib/scribble/scribble-common.js b/pkgs/scribble-pkgs/scribble-lib/scribble/scribble-common.js index efbba09774..c0a32af9a5 100644 --- a/pkgs/scribble-pkgs/scribble-lib/scribble/scribble-common.js +++ b/pkgs/scribble-pkgs/scribble-lib/scribble/scribble-common.js @@ -20,7 +20,7 @@ var page_args = function GetPageArg(key, def) { for (var i=0; i