Subject: Re: bug#42633: 8.32 make check as root failure of rmdir/ignore.sh
From: Bernhard Voelker <[email-masked]>
To: Pádraig Brady <[email-masked]>, Nick Alcock <[email-masked]>, [email-masked]
Date: Mon, 10 Aug 2020 22:29:39 +0200
List-Id: <debbugs-submit.debbugs.gnu.org>

On 2020-08-03 22:07, Bernhard Voelker wrote:
> Pushing soon ... unless there are objections.

Pushed some days ago, and therefore I'm hereby marking this issue as done.

Have a nice day,
Berny