diff options
| author | Guillaume Melquiond | 2014-06-26 17:37:29 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-06-26 17:37:29 +0200 |
| commit | cda7b80182b03c7b04baf5cc2cc6aa33984e054a (patch) | |
| tree | 75b1be4215f786ab56c3fcc6184b46867444d0f7 /kernel/type_errors.mli | |
| parent | f27134ab2cf4fa1ddc1dd19b2b961e3c3ed040ff (diff) | |
Avoid scanning .coq-native directories when building the library index.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions