diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 13:40:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 13:40:28 +0200 |
| commit | 1c5f120fba49b397aad7b8c07dcc10cec1cfc026 (patch) | |
| tree | dd6c4772165cdc4f546105c5486476611d34c9b9 /dev/build/windows/CAVEATS.txt | |
| 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/CAVEATS.txt')
0 files changed, 0 insertions, 0 deletions