On Friday, July 17, 2020, Andy Fan <zhihui(dot)fan1213(at)gmail(dot)com> wrote:
>
>
> On Sat, Jul 18, 2020 at 12:23 AM David G. Johnston <
> david(dot)g(dot)johnston(at)gmail(dot)com> wrote:
>
>>
>> - which they still need to be aware of even though this patch removes one
>> situation where it matters.
>>
>
> Can you provide an example of this? If it is not very troublesome, I'd
> like to fix both.
>
Nothing concrete off hand, more of an impression.
David J.