diff options
| author | Maxime Dénès | 2018-03-16 15:44:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-16 15:44:52 +0100 |
| commit | fa84854ad1376d790739eb58d9d85d6864373ef8 (patch) | |
| tree | d5881943d0549f89810d1fc8d7ea2ffb938222bf /dev/doc | |
| parent | 8f3717845f5fa3bebddfe5246f4646bc062ac244 (diff) | |
| parent | efcff2e4ae6cabaf90fec1d5bd0cec0f5d4a3a4a (diff) | |
Merge PR #7005: Fix coqtop timeout
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions