On Wednesday, January 10, 2018 9:53:07 AM CET Paul Eggert wrote: > No further comment, so I installed the proposed patches and I'm closing this > bug report.
Sorry. There were just too many changes in your patches for me to review them quickly enough (and most of the changes were unrelated to my initial submission anyway). Thank you for fixing it! Kamil
