diff --git a/collects/scribblings/main/private/search.js b/collects/scribblings/main/private/search.js index 2baa444262..e0aeda00aa 100644 --- a/collects/scribblings/main/private/search.js +++ b/collects/scribblings/main/private/search.js @@ -599,6 +599,7 @@ function UpdateResults() { if (first_search_result < 0 || first_search_result >= search_results.length) first_search_result = 0; + var link_lang = (cur_plt_lang && ("?lang="+escape(cur_plt_lang))); for (var i=0; i'; + var href = UncompactUrl(res[1]); + if (link_lang) { + var hash = href.indexOf("#"); + if (hash >= 0) + href = href.substring(0,hash) + link_lang + href.substring(hash); + else + href = href + link_lang; + } result_links[i].innerHTML = - '' + '' + UncompactHtml(res[2]) + '' + (note || ""); result_links[i].style.backgroundColor = (n < exact_results_num) ? highlight_color : background_color;