diff options
| author | Emilio Jesus Gallego Arias | 2019-01-28 13:14:44 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-28 15:28:33 +0100 |
| commit | da420fd8315db308a013bb3cca3512fd9c9bf627 (patch) | |
| tree | bbc478d4c84bbcc6010f6f33570f2b6bf99df63a /engine/termops.ml | |
| parent | 9d9bc6fa0eb3d83218f7ed025cacab4875e555ea (diff) | |
[vernac] Fix classification of `Declare Custom Entry`
It seems that this command should be classified as modifying the parser.
Fixes #9419
Thanks to @gares
Diffstat (limited to 'engine/termops.ml')
0 files changed, 0 insertions, 0 deletions