diff options
| author | Maxime Dénès | 2017-09-27 00:38:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-27 00:49:51 +0200 |
| commit | 77d95ecd65a6bbebfcd89193fb3e2c43ebc6469a (patch) | |
| tree | 8424d2ec39f0ac2e1fa598f0d2208954389eed61 /dev/ci/ci-basic-overlay.sh | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
Avoid looping when searching for CoqProject.
This could happen with paths on Windows, or even relative paths on all
OSs.
Fixes #5730: CoqIDE becomes unresponsive on file open.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions