diff options
author | Eelco Dolstra <edolstra@gmail.com> | 2020-12-09 12:40:00 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-09 12:40:00 +0100 |
commit | 253571e4ecc990c7f63ed8d70dbee9e4cec8002c (patch) | |
tree | 69b3a119773dd20b2ba239eb2160c76251f09375 /scripts | |
parent | eb458ad1b2d5ef316fe8948d4e1abd484dde41eb (diff) | |
parent | c87267c2a4621a42d6bfcdb7944cd546f194787a (diff) |
Merge pull request #4342 from tweag/fix-remote-build-hook
fix remote build hook
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions