diff options
| author | MilanVasko | 2022-07-27 09:02:19 +0000 |
|---|---|---|
| committer | GitHub | 2022-07-27 09:02:19 +0000 |
| commit | 9a496237215dc09ef8f639fc79f7e63e2309c080 (patch) | |
| tree | 744f81d351a48fe5eb2b2022fc712dd64f1d4ce4 /book/src | |
| parent | 846a6b65c3d13f49b571beee2189d17b71c92e3f (diff) | |
Use OR of all selections in search_selection command (#3138)
Closes #2312
Diffstat (limited to 'book/src')
0 files changed, 0 insertions, 0 deletions