From 96fc0407d0b8119f68030f834ed2b2af26161825 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). original commit: d1525edf62a1db2ade3c64dd17eb81bff87a4112 --- 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 efbba097..c0a32af9 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