aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-27 17:15:10 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-29 17:55:31 +0200
commitedb55a94fc5c0473e57f5a61c0c723194c2ff414 (patch)
treed5949e1815b62e5cd1966d2930e375c1d224aa22 /.gitignore
parent89c2942352ec5d8d5b9cfe1116376412770cb396 (diff)
Fix bug #4798: compat notations should not modify the parser.
This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions