Skip to content

Plugins should end .exe on Windows#4709

Merged
dra27 merged 1 commit intoocaml:masterfrom dra27:plugins-exeJun 11, 2021

Commits

Commits on Jun 10, 2021