diff options
| author | github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> | 2024-01-08 20:57:39 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-01-08 20:57:39 +0100 |
| commit | 4dd5171652018e29bf9e496522df3be51d615a2c (patch) | |
| tree | cd820d07d3b70b7149f928fc18cba7f36587a7ff /src | |
| parent | 4a1c3762df03fd20518f7aef25ee1027ac235032 (diff) | |
fix an old lost direct (#9717)
this part must have been moved quite a while ago, but apparently so far
no one noticed
(cherry picked from commit 6db805b3d1e4eccd0103d9856b8ab3d01efba51f)
Co-authored-by: Valentin Gagarin <valentin.gagarin@tweag.io>
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions