diff options
| author | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-19 16:26:24 +0200 |
| commit | 8bd60579d4768793c849b9b4cd46f14d33d0f71d (patch) | |
| tree | 9fb0510584dae4f5416f8776b26cd7964ceb810f /dev/base_include | |
| parent | e3e8dfb4c2f30ed1c6715999e1f74914e7bc187b (diff) | |
| parent | feb9c50b5812a01e9dc60e2408f4f9f38986ce8c (diff) | |
Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions