diff options
| author | coqbot-app[bot] | 2021-01-28 21:20:59 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-28 21:20:59 +0000 |
| commit | ed29e0913742c307175846557ed8390a8da771e3 (patch) | |
| tree | e086e1cecc69e532686cf6d6c3de8a422638e6f5 /dev/include | |
| parent | 59dc4eb40e9512d95f73df7a6bc67edcb1907acd (diff) | |
| parent | de7f7fe34828debfa4bd5130810ee5ccc0ea0170 (diff) | |
Merge PR #13789: Document limitation of rewrite regarding occurrence selection.
Reviewed-by: jfehrle
Reviewed-by: silene
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions