On Sun, 23 Dec 2018 at 14:39, Nico Huber email@example.com wrote:
When we switched to Gerrit, we decided to still allow patches per email and also on GitHub. Though, all patches have to go through Gerrit in the end as that's where the official repository is.
Okay, I guess I'll add that to my "to learn" for 2019.
I'll leave some comments their and pull those commits that seem ready to go.
I've rebased that warnings branch (which updates the github PR). Feel free to cherry pick any or all of those patches in the meantime. Thanks.