Jeremy Bicha Mon, 11 Jul 2016 19:22:01 -0700
Hi, it's been a month with no response. How about I just push this minor patch to collab-maint git?
Thanks, Jeremy