On Tue, May 19, 2020 at 06:46:14PM +0200, Pierre Neidhardt wrote:
> Should I file a bug?

I've done it: <https://bugs.gnu.org/41406>

Reply via email to