Commit 558ca830 authored by Albert Gräf's avatar Albert Gräf
Browse files

Fix case-sensitive search in the browser's findbox.

This uses findAndReplaceDOMText(), which apparently looks for
case-sensitive matches, but the search text entered by the user is
*always* converted to lowercase. This means that mixed case search terms
just won't be found, which is bad. (E.g., try searching for "GEM" in the
toc to see this bug in action.)

Fixed by just removing the call to toLowerCase() on the search text,
case-sensitive searches now work as expected, problem solved.
parent 5f9e9435
......@@ -500,7 +500,7 @@ function console_find_text(elem, evt, callback) {
} else {
window.findAndReplaceDOMText(console_text, {
//preset: "prose",
find: elem.value.toLowerCase(),
find: elem.value,
wrap: wrap_tag
// The searchAndReplace API is so bad you can't even know how
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment