Paul Eggert Sun, 20 Nov 2016 00:36:07 -0800
No further comment and it has been a while, so closing the bug.
