diff options
| author | Emilio Jesus Gallego Arias | 2018-02-06 21:39:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-09 23:53:21 +0100 |
| commit | c0e99b45a97aa0d506e32d1daeb594c372ea82fa (patch) | |
| tree | 8cae79e105967ad260deacedec3d8b35744e9b08 /kernel/cemitcodes.ml | |
| parent | 79bb4a67a96ec28998d070e405c18fd5fd29d6fb (diff) | |
[vernac] Fix outdated comment.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions