On Sat, Jun 08, 2019 at 10:24:39AM +0900, Michael Paquier wrote:> Indeed, this makes the header more consistent. Thanks for noticing.
Double-checked the surroundings, and done.--Michael