diff options
| author | Vincent Laporte | 2019-03-26 08:46:48 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-26 08:46:48 +0000 |
| commit | 9788d6d3b2799e5aeabaa4fbde9ae50d71f8b39b (patch) | |
| tree | 157b7392b32cae1c10ec06d2963c1bdd7319946c /dev | |
| parent | 6e6844e89bdf57f00bc1e4d3de110ca45d0b51bf (diff) | |
Fix for https://github.com/coq/coq/pull/8984
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions