On Tue, 20 Mar 2018 09:42:13 +0800 Sepherosa Ziehau <sepherosa at gmail.com> wrote: > I think it has been fixed on master. Well, I'm on fairly up-to-date master... Was it some recent commit? Thank you. -- Daniel