diff options
| author | Pierre-Marie Pédrot | 2016-01-24 12:35:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-24 12:37:38 +0100 |
| commit | cb30837323aa462df24ad6668790f67b9bf20b5d (patch) | |
| tree | 58f171b3ac23b52abecb5617fad57cab29d6f41f /kernel | |
| parent | 4b1103dc38754917e12bf04feca446e02cf55f07 (diff) | |
Fixing bug #4495: Failed assertion in metasyntax.ml.
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions