diff options
| author | Pascal Kuthe | 2023-02-02 19:48:16 +0000 |
|---|---|---|
| committer | GitHub | 2023-02-02 19:48:16 +0000 |
| commit | f0c2e898b49b2392d6d1ca02680e88b90e62017e (patch) | |
| tree | 89005801fce37a4817e737c401b18c0553b9ff8b /runtime/queries/lean | |
| parent | e31943c4c4a996da1fe8704db052c7d44984fcc4 (diff) | |
add substring matching options to picker (#5114)
Diffstat (limited to 'runtime/queries/lean')
0 files changed, 0 insertions, 0 deletions