diff options
| author | Gaëtan Gilbert | 2020-04-17 11:16:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-17 11:16:28 +0200 |
| commit | 633b462dc0c0211d353faebc6acbe6393c1566b6 (patch) | |
| tree | 9324c8a5eab5576c74d088e07c506f6e8604cfb7 /vernac/comProgramFixpoint.ml | |
| parent | b543bf9c65c98baf90a605b5545dd6315fd2f261 (diff) | |
CI: Ignore spurious errors in validate jobs
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions