diff options
| author | Hugo Herbelin | 2019-01-10 23:24:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-01-22 15:09:08 +0100 |
| commit | 03a50923af6fec0deb0c3c2218656bfb74341e47 (patch) | |
| tree | fef135ed428ef0851234e9066ccd05a1bd83d96b /dev | |
| parent | d88f9883ce8313c82cb081987e30de1d7201805e (diff) | |
Fixing #9329 (registering empty levels in the order they are recomputed).
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions