scala/scala — pull request #3055 by Jentsch (2013-10-18 22:31:45+00:00)
Title: Prevent useless filter refresh in docs

Hi,
this deals with the scala doc JS.

Currently if you type a key inside the input field top left, the list below will be recalculated. This happens even if the input doesn't change (e.g. pressing shift or moving with arrow keys). Since the list could be very long this action takes some time and is a little bit annoying.

I added some lines (3) inside the JS of the scala doc generator to prevent that the filter operation if the field stays unchanged.

Also under: https://groups.google.com/forum/#!topic/scala-internals/Y1MdwOxhjZo
I hope you like this very minor change.