Do not pass the -toolchain option when building a plugin#160
Merged
gasche merged 1 commit intoocaml:masterfrom Feb 28, 2017
whitequark:no-toolchain-for-plugin
Merged
Do not pass the -toolchain option when building a plugin#160gasche merged 1 commit intoocaml:masterfrom whitequark:no-toolchain-for-plugin
gasche merged 1 commit intoocaml:masterfrom
whitequark:no-toolchain-for-plugin
