diff options
| author | Maxime Dénès | 2019-01-18 16:09:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-19 15:05:14 +0100 |
| commit | 1e0d3028402080d449ce5a84bf20cba221cc8f0b (patch) | |
| tree | b92691701f6c29c0a49a68429f9137ba15166247 /dev/ci | |
| parent | b2877df2c79147bd2e26e53e43291b9b29a2aab8 (diff) | |
Fix recursive loadpath of ML files
ML files at the root were not taken into account. Coqdep was already
doing the right thing.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions