diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-20 11:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-20 11:14:09 +0200 |
| commit | 62684a5c817da4afc2a7dac6ece03facabdd5fe4 (patch) | |
| tree | 224a8c854062bcd75add73f0a95a40223239acd1 /plugins/ltac/tacentries.mli | |
| parent | 025a60b92618e4a8f10ab9704a38949383c87efa (diff) | |
| parent | 8df509882d5b0954b40b576c4e9d3b3f742c619d (diff) | |
Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than just Iris
Diffstat (limited to 'plugins/ltac/tacentries.mli')
0 files changed, 0 insertions, 0 deletions