diff options
| author | Teddy Wing | 2021-06-24 20:51:31 +0200 |
|---|---|---|
| committer | Teddy Wing | 2021-06-24 20:53:34 +0200 |
| commit | 98ec0eb9370bd12225fde1d8c2ff8b8ace693609 (patch) | |
| tree | 69f461278fed740aa6cfadbd4ac3ae506dc5f1f2 /src/github.rs | |
| parent | b3d87f44a9801ea84347dee764d21c0db8d87fbd (diff) | |
| download | reflectub-98ec0eb9370bd12225fde1d8c2ff8b8ace693609.tar.bz2 | |
git::mirror(): Change HEAD to GitHub default branch
The default branch after mirroring was typically 'master'. On GitHub,
the default branch may not necessarily be 'master'. Change the default
branch by changing the HEAD to GitHub's default branch so that the
mirrored repository better matches GitHub.
We'll also need to make a change to the update function in case the
default branch changes after mirroring.
Diffstat (limited to 'src/github.rs')
0 files changed, 0 insertions, 0 deletions