diff options
| author | Nadrieril | 2020-11-02 21:59:26 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-02 21:59:26 +0000 |
| commit | 2839bfe23b7a0916e9e625a4d62835c39d8693ba (patch) | |
| tree | 7ef219fca84adc5ed2e931f610a27c65dc33749d /dhall/src/operations | |
| parent | 34d92560a0a2124e5eadea4832795874505b6cc5 (diff) | |
| parent | e4638e257823e01408ac46211764470ec565f964 (diff) | |
Merge pull request #195 from basile-henry/workaround-clippy-issue
CI: Use a workaround to not hit the clippy issue
Diffstat (limited to 'dhall/src/operations')
0 files changed, 0 insertions, 0 deletions