On Sat, Jul 04, 2020 at 09:17:52PM +0200, Juan José Santamaría Flecha wrote: > Going through the open items in the commitfest, I see that this patch has > not been pushed. It still applies and solves the warning so, I am marking > it as RFC.
Thanks, applied. I was actually waiting to see if you had more comments.
> Adding a help option is a new feature, that can have its own patch without > delaying this one any further.
Yep. And I am not sure if that's worth worrying either. -- Michael