On Wed, Oct 3, 2018 at 9:04 AM Dean Rasheed <dean.a.rash...@gmail.com> wrote: > > On Thu, 27 Sep 2018 at 14:22, Dean Rasheed <dean.a.rash...@gmail.com> wrote: > > I'll post an updated patch in a while. > > > > I finally got round to looking at this again. Here is an update, based > on the review comments. > > The next question is whether or not to back-patch this. Although this > was reported as a bug, my inclination is to apply this to HEAD only, > based on the lack of prior complaints. That also matches our decision > for other similar patches, e.g., 7d9a4737c2.
This diff looks good to me. Also, it applies cleanly against abd9ca377d669a6e0560e854d7e987438d0e612e and passes `make check-world`. I agree that this is not suitable for a patch release. Madeleine
