diff options
| author | Jonathan LEI | 2023-01-23 13:51:34 +0000 |
|---|---|---|
| committer | GitHub | 2023-01-23 13:51:34 +0000 |
| commit | 769fb5fe97ac321ba030ac8fbf7e3793700f282c (patch) | |
| tree | 1adf028c23781487befc02eb9fa3e093c174a54f /runtime/queries/lean | |
| parent | 5c6b7127f88ef7508cefec74e2dc6479e1cfa609 (diff) | |
Make clippy happy on Windows (#5644)
Diffstat (limited to 'runtime/queries/lean')
0 files changed, 0 insertions, 0 deletions