tree 6a41c218446e6798f526293d6a41857fb453ff78
parent 944485e01babf7839732f42be1503e6ecc64a289
author Luca Milanesio <luca.milanesio@gmail.com> 1463524659 +0100
committer Luca Milanesio <luca.milanesio@gmail.com> 1479278243 +0000

Add plugins search box on the top navigation bar

Introduce a top search box to be able to filter the list of plugins.

Specifying a search keyword helps a lot on focusing on what the
administrator is looking for, without having to go through an
alphabetical long list.

Change-Id: I5af06c87c7d1232368bd52ff7ecc000924835824