diff options
| author | Maxime Dénès | 2018-06-21 17:40:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-21 17:40:13 +0200 |
| commit | 41cf6afdb70b073838bd2a1e71f76c600e03c006 (patch) | |
| tree | ac599113aa91feef19fa1d59feeaa27a685ce360 /dev | |
| parent | be6f66e3d4424b0dfbbbe3097a617aebb8aefca2 (diff) | |
| parent | 3d8342c2c26f710583e6b9246bd1069cb8b42d7d (diff) | |
Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions