Write mdx files to .mdx dir to avoid running mdx as part of @all#3659

Merged

NathanReb merged 1 commit intoocaml:masterfrom NathanReb:fix-mdx-hint

Jul 30, 2020

+13-6

Commits on Jul 30, 2020

Write mdx files to .mdx dir to avoid running mdx as part of @ALL
NathanReb
committed