Add filtering for the repository selector.

Review Request #4526 — Created Sept. 4, 2013 and submitted — Latest diff uploaded

Information

Review Board
master

Reviewers

Add filtering for the repository selector.

This change adds a search box for the repository list, which should help for
servers that have a ton of repos connected.

  • Tested the animation back and forth to make sure everything was silky smooth
    and drew correctly.
  • Added a couple repositories with different names. Checked that searches
    worked as expected.
  • Ran jshint.