diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss
index 325bcd3750..081f7ac23c 100644
--- a/collects/scribblings/main/private/make-search.ss
+++ b/collects/scribblings/main/private/make-search.ss
@@ -123,13 +123,14 @@
// Globally visible bindings
var key_handler, toggle_help_pref, hide_prefs,
- set_results_num, set_highlight_color;
+ set_results_num, set_type_delay, set_highlight_color;
(function(){
- // Configuration options
- var results_num = (GetCookie("PLT_ResultsNum", false) || 20);
- var highlight_color = (GetCookie("PLT_HighlightColor", false) || "#ffd");
+ // Configuration options (use || in case the cookie exists but empty)
+ var results_num = (GetCookie("PLT_ResultsNum", false) || 20);
+ var type_delay = (GetCookie("PLT_TypeDelay", false) || 300)
+ var highlight_color = (GetCookie("PLT_HighlightColor", false) || "#ffd");
var background_color = "#f8f8f8";
var query, status, results_container, result_links,
@@ -165,6 +166,10 @@
+'
'
+ +'Type delay:'
+ +'
'
+'Exact matches color:'
+'