On Fri, Dec 04, 2020 at 09:05:49AM +0100, Konrad Hinsen wrote: > Hi Robert, > > >> > The bug: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=26981 > >> > If I don't hear back I'll assume it's safe to close this. > >> > >> Yes, it is. Thanks for doing a cleanup! > > > > This bug report is still relevant? Or are you saying that it is fixed? > > Sorry if my email was a bit ambiguous! > > Right. My full answer is "Yes, it is safe to close this."
Closing...
