Paul Eggert <eggert@cs.ucla.edu> schrieb am Sa., 20. Mai 2017 um 22:23 Uhr:

Thanks. These patches all look good; please commit. For routine stuff like this
you might consider saving us all some time and just committing it.

Sure, will do.