diff options
| author | Théo Zimmermann | 2020-04-17 14:32:02 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-17 14:32:02 +0200 |
| commit | f3af9a4c6e6813f32dfe632209e145ffbf5fed98 (patch) | |
| tree | 44632df517b713a6bd487445e433dab9b9d98e16 /vernac/comProgramFixpoint.ml | |
| parent | 87f8c9fce73ebf8bc0b6cb53536bdb3861f09e41 (diff) | |
| parent | 633b462dc0c0211d353faebc6acbe6393c1566b6 (diff) | |
Merge PR #12111: CI: Ignore spurious errors in validate jobs
Reviewed-by: Zimmi48
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions