diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-06 20:45:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-06 20:47:34 +0200 |
| commit | f4de78b048f6567f1e1fdd553b4f7ada0e0707b8 (patch) | |
| tree | d4c52d65d5d9cb55f98ed2710dc42344c0b93baf /kernel/declareops.ml | |
| parent | d180279aa934dfbb3fd97e707675b55f464f14ef (diff) | |
Do not add "Append" as a lexer keyword.
This was introduced to implement the Append feature on options. As usual when
messing with predefined keywords, this broke code in the wild. In order not
to create a new keyword, we do the string analysis on the production branch of
parsing.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions