Re: [egit-dev] Re: [jgit-dev] Font sizes in gerrit

[Shawn Pearce <spearce@xxxxxxxxxxx>]

On Mon, Mar 1, 2010 at 10:15 AM, Shawn O. Pearce <spearce@xxxxxxxxxxx> wrote:
> Alex Blewitt <alex.blewitt@xxxxxxxxx> wrote:
>> I'd say ditch the header. It's always in the way for me at various
>> places and doesn't really fit well even without the font size.
>
> I can't.  EMO wants it.

Another option is to try and do what DMDirc did:

http://gerrit.dmdirc.com/#patch,sidebyside,932,2,src/com/dmdirc/parser/common/IgnoreList.java

Basically they used CSS to force the header element that is below the
Gerrit menu bar to be above it.  But that looks like they are again
relying on pixel counts to make it work.