On Wed, Jun 05, 2019 at 05:14:01PM +0200, Ludovic Courtès wrote:
> I can’t comment about the GNOME Help issue, but otherwise the patch
> LGTM.
> 
> Thanks!

Okay, pushed as ff22ff42a1d759eafd94e596c7a610e8fd9eb001

Thanks for the review!