diff options
| author | Maxime Dénès | 2017-10-03 15:34:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-03 15:34:46 +0200 |
| commit | 90c4339a54e392b4564c9851fbd48fe910bb4cab (patch) | |
| tree | dd01d9bbc9ed985d048f1e95fedbe11ba19ff5b3 /dev | |
| parent | 3a8209d262ef586baee5b76161afd83893d1dad3 (diff) | |
| parent | 77d95ecd65a6bbebfcd89193fb3e2c43ebc6469a (diff) | |
Merge PR #1100: Avoid looping when searching for CoqProject.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions