In the meantime -- I looked at a slightly different way of fixing this. Padding between widgets in the header looked a little unusual to me anyway; so I added 5 pixels on top and bottom; then pushed the result to my PPA. If someone wants to try it and review whether it makes things better or not:
In the meantime -- I looked at a slightly different way of fixing this. Padding between widgets in the header looked a little unusual to me anyway; so I added 5 pixels on top and bottom; then pushed the result to my PPA. If someone wants to try it and review whether it makes things better or not:
https:/ /launchpad. net/~mathieu- tl/+archive/ ppa/+sourcepub/ 2495974/ +listing- archive- extra
Just a workaround, but the change with 10px (although that's arguably a lot) seems to work properly at multiple font sizes.