On Sat, Jan 18, 2020 at 6:11 PM Karl Berry <k...@freefriends.org> wrote: > Here's my proposed patch to use chmod and rm -rf (again), instead of > deltree.pl. > > In the verbose output in case of failure, I split the difference and > added a terminating line "end ls ...", but did not prefix the ls > output. While I was testing, that seemed the most usable.
Thanks, Karl. That looks fine. In the log, please use the short bug URL: https://debbugs.gnu.org/39078 rather than: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=39078