diff options
| author | Maxime Dénès | 2019-12-19 12:45:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-12-20 13:27:13 +0100 |
| commit | 7149fef354d55f4b5012eac7efa15b4e7bac3d38 (patch) | |
| tree | ab27bfa6035490d65205702854d34dd16411c029 /lib/flags.ml | |
| parent | 5c667d56cd0a441f787019aef44bf18bec9c7b20 (diff) | |
Fix handling of recursive notations with custom entries
Fixes #9532
Fixes #9490
Diffstat (limited to 'lib/flags.ml')
0 files changed, 0 insertions, 0 deletions