diff --git a/collects/scribblings/main/private/search.js b/collects/scribblings/main/private/search.js index 999009634a..6fe21b2e81 100644 --- a/collects/scribblings/main/private/search.js +++ b/collects/scribblings/main/private/search.js @@ -439,20 +439,21 @@ function Search(data, term, is_pre, K) { var r, min = C_max, max = C_min; for (var j=0; j= C_rexact && min >= C_exact) exacts.push(data[i]); else if (min > C_wordmatch) matches.push(data[i]); else if (min > C_fail) wordmatches.push(data[i]); fuel--; i++; } - if (i