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

Reply via email to