Hey @Kladar and @avila196 - I’m taking a look at this now. It’s obviously a trivial change; the question is, will it have other consequences that we’re not considering?
I’ll do a bit more research - but the plan right now is to merge this change in the next 2 weeks.