Francois Ferrand d8cca59ecb Merge top menu items contributed by plugins ...

Each plugin contributes a list single of menus, which are expected
to be merged in existing top menu entries if they already exist:
as stated in the doc and already implemented in GWT:

 "Plugins can also add additional menu items to Gerrit’s top menu
  entries by defining a MenuEntry that has the same name as a Gerrit
  top menu entry"

Change-Id: I8540b93b71e9c9c1f043e16d2076bade4de9a49a

2019-01-04 17:09:21 +00:00

..

gr-main-header_test.html

Merge top menu items contributed by plugins

2019-01-04 17:09:21 +00:00

gr-main-header.html

Replace Roboto-Medium font with Roboto and font weight.

2018-10-01 10:35:17 -07:00

gr-main-header.js

Merge top menu items contributed by plugins

2019-01-04 17:09:21 +00:00