Subject: Re: bug#24714: delete-directory race condition

From: Paul Eggert <[email-masked]>
Date: Tue, 18 Oct 2016 09:44:56 -0700

Although I didn't reproduce the bug, I changed delete-directory 
according to Eli's suggestion by installing the attached patch into 
master. Glenn, can you please try it in your environment?