Skip to content

Add --disable-promotion option#2588

Merged
rgrinberg merged 2 commits intoocaml:masterfrom rgrinberg:turn-off-promotionAug 27, 2019

Commits

Commits on Aug 27, 2019