diff options
| author | coqbot-app[bot] | 2020-10-20 14:15:40 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-20 14:15:40 +0000 |
| commit | 91e7863e64a5741b6530828c1642d765ddff41ae (patch) | |
| tree | 6ee9e729905a50b4351ada1f822d3dcce5edeb6c /kernel | |
| parent | 554bdc2df7e5b63bbf6fcc60c33437842d2f5541 (diff) | |
| parent | 48e0d4112cdf23ec89e8044387bd8484cb026b92 (diff) | |
Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loop
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions