Workaround for name clash caused by riot at minttea's site?

[glyh]

See this riot-ml/riot#19.
I run into this when using both mintea and janestreet's core.

[leostera]

Thanks for reporting @glyh! We'll bump this on the Riot side.