diff options
| -rw-r--r-- | html/haddock-util.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/html/haddock-util.js b/html/haddock-util.js index ddc7f6d0..e5d6977e 100644 --- a/html/haddock-util.js +++ b/html/haddock-util.js @@ -15,7 +15,7 @@ function toggle(button,id) } -var max_results = 50; +var max_results = 75; // 50 is not enough to search for map in the base libraries var shown_range = null; var last_search = null; |