diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 14:05:36 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-31 00:58:15 +0200 |
commit | aa1565a20f6c42ba28a9346ee25404d893946c5d (patch) | |
tree | fce245a4f7d2205e859b460459306de9f3b3e283 /vernac/vernacentries.ml | |
parent | d4def32456c0fadb7fc9814af7e7b2b21a37f0a6 (diff) |
Linter: verify overlay extensions.
Diffstat (limited to 'vernac/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions