diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-09 08:18:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-09 08:48:13 +0200 |
| commit | eb87cdaeb252d758b6a76b36867254823169576b (patch) | |
| tree | 2b1345ba106bd75c6c889524d616ef1062b20237 /toplevel/metasyntax.mli | |
| parent | 0a6f0c161756a1878dd81e438df86f08631d8399 (diff) | |
A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).
More precisely, commands that calls parse_entry put the lexer in an
inconsistent state, breaking the lexing of bullet which relies on it.
(Not to be pushed to v8.6 which has a better fix).
Diffstat (limited to 'toplevel/metasyntax.mli')
0 files changed, 0 insertions, 0 deletions