Nick Dokos <ndokos <at> gmail.com> writes: > > I pushed the obvious fix for this to master. >
As a bugfix, this should have gone to maint and then merged into master. Now you'll need to cherry-pick it onto maint and get a duplicate commit. Regards, Achim.
