diff options
| author | Gaëtan Gilbert | 2020-11-24 15:04:05 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-24 15:04:25 +0100 |
| commit | c3b260cfd5e74501aa0101b9e75f050bd6a3566d (patch) | |
| tree | 0e6a09b1cb560c13f0569c008c31df940885dabc /interp | |
| parent | 94d579844817edcbb2454dd9dc79071b2cd1d12a (diff) | |
Fix linter: incorrect commit was picked in CI
The bot merge was changed some time ago.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions