diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-08 23:38:32 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-08 23:38:32 +0100 |
commit | c671d86beecb4e31ad5c7752f7e4fb570823e837 (patch) | |
tree | 198cfdd80f336c585fef35aa94ba60c0ab5b8b2c /vernac/declareDef.ml | |
parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) |
Cleanup conditional in lint-repository.sh
Diffstat (limited to 'vernac/declareDef.ml')
0 files changed, 0 insertions, 0 deletions