diff options
| author | Pierre-Marie Pédrot | 2020-04-23 14:49:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-23 14:49:58 +0200 |
| commit | 7863c12930687e1e2dc982d9b406fb4d6e7a02c1 (patch) | |
| tree | 957bd8b46b1c2d9dbbd4fbb25fa0877cb2aae278 /engine | |
| parent | 7e2167f5bfd7d70847d1b1ece34c1f0303f46fc8 (diff) | |
| parent | 21a4d14307a9590c6b70e22383f96679012b5f4d (diff) | |
Merge PR #12083: Tweak ltac2 grammar to make doc_grammar happy
Reviewed-by: ppedrot
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions