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>
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>