Hi, it's been a month with no response.

How about I just push this minor patch to collab-maint git?

Thanks,
Jeremy

Reply via email to