On Tue, 20 Mar 2018 09:42:13 +0800 Sepherosa Ziehau <[email protected]> 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
