diff options
author | 2018-05-16 13:40:28 +0200 | |
---|---|---|
committer | 2018-05-16 13:40:28 +0200 | |
commit | 1c5f120fba49b397aad7b8c07dcc10cec1cfc026 (patch) | |
tree | dd6c4772165cdc4f546105c5486476611d34c9b9 /dev/build/windows/MakeCoq_86git_installer.bat | |
parent | 3f480c993311d19b152deb6bb4dc561188d76fc7 (diff) |
[windows] Don't make menhir and int anymore.
As pointed out by @MSoegtropIMC
[here](https://github.com/coq/coq/pull/7522#issuecomment-389478963)
there are not needed to build the packages, so not building them will
save a couple of minutes.
Diffstat (limited to 'dev/build/windows/MakeCoq_86git_installer.bat')
0 files changed, 0 insertions, 0 deletions