| commit | 5f2fff3ec60e0f1537eb748da4b4c79994731360 | [log] [tgz] |
|---|---|---|
| author | Luca Milanesio <luca.milanesio@gmail.com> | Tue May 17 23:37:39 2016 +0100 |
| committer | Luca Milanesio <luca.milanesio@gmail.com> | Wed Nov 16 06:37:23 2016 +0000 |
| tree | 6a41c218446e6798f526293d6a41857fb453ff78 | |
| parent | 944485e01babf7839732f42be1503e6ecc64a289 [diff] |
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