On Wed, 4 Aug 2021 at 00:02, David Rowley <dgrowle...@gmail.com> wrote:
> Yeah, I think it can be safely removed.  I can do so unless someone
> thinks otherwise.

Pushed.

David


Reply via email to