On Mon, Nov 6, 2017 at 9:36 PM, MauMau <maumau...@gmail.com> wrote: > From: Thomas Munro > With your v2 patch "make docs" fails. Here is a small patch to apply > on top of yours to fix that and some small copy/paste errors, if I > understood correctly. > > Ouch, thanks. I'd like to merge your fix when I submit the next > revision of my patch.
This thread is waiting at least for a new version, which has not happened in three weeks. so I am marking it as returned with feedback for now. -- Michael
