On 8/31/20 12:13 PM, Helge Kreutzmann wrote:
> But, actually, personally I would not change it, I think the previous
> order looks better.

OK, let's leave that alone then.

The remaining proposed changes are to use bold rather than italics for command 
names so I installed the attached to do that. Closing the bug report.