On Wed, Oct 3, 2018 at 9:04 AM Dean Rasheed <dean.a.rasheed@gmail.com> wrote:
>
> On Thu, 27 Sep 2018 at 14:22, Dean Rasheed <dean.a.rasheed@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
