diff options
| author | Théo Zimmermann | 2017-12-08 10:50:09 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-12-08 10:50:09 +0100 |
| commit | 2434e85e1f2006e66efd74bd6cd7224e301e3bff (patch) | |
| tree | 9bfe4e232a648b38e283f30952cc38cb7dd85226 /kernel/cemitcodes.ml | |
| parent | 437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (diff) | |
Fix a copy-paste error in ci-ltac2.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions