diff options
| author | Maxime Dénès | 2017-10-20 11:14:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-20 11:14:18 +0200 |
| commit | 0897d0f642c19419c513f9609782436bebf28f5b (patch) | |
| tree | 32ba56bfcb1e90876b5c47769c1224e878060222 /plugins | |
| parent | 62684a5c817da4afc2a7dac6ece03facabdd5fe4 (diff) | |
| parent | 2f4b474295699936bb80f864711ea31a6d24ae38 (diff) | |
Merge PR #5989: Handle ∞ in coq-makefile timing test-suite
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions