On Wed, Apr 03, 2019 at 11:36:26PM +0200, Patrice Dumas wrote: > With the change I did it is not needed anymore for those commands to be > in global commands. I think that they should actually be removed from > the global commands.
Okay, done. Removed in commit 2045547. > > -- > Pat
