diff options
| author | Eelco Dolstra <edolstra@gmail.com> | 2021-09-14 13:38:45 +0200 |
|---|---|---|
| committer | Eelco Dolstra <edolstra@gmail.com> | 2021-09-14 13:38:45 +0200 |
| commit | 07996c481081d729d3ff1a53932e66c713ef5af2 (patch) | |
| tree | 00551b80f8f1dd184c8f117bf6d0daa6685d93ea /.github | |
| parent | d72d31d5294586943ef9fb7d13706f629837bf21 (diff) | |
github fetcher: Don't use HEAD branch when cloning
Fixes #4394.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions