diff options
| author | Emilio Jesus Gallego Arias | 2018-05-16 13:40:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-16 13:40:28 +0200 |
| commit | 1c5f120fba49b397aad7b8c07dcc10cec1cfc026 (patch) | |
| tree | dd6c4772165cdc4f546105c5486476611d34c9b9 /kernel/cbytecodes.mli | |
| 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 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions