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

[glyh]

See this https://github.com/riot-ml/riot/issues/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.