diff options
| author | Teddy Wing | 2021-06-24 21:18:07 +0200 |
|---|---|---|
| committer | Teddy Wing | 2021-06-24 21:18:07 +0200 |
| commit | 85df39e199fa146e22d9cf8ccd635277fe066d12 (patch) | |
| tree | ebed651a7cdb1059ca92ca0916196c2dc19c27f3 /src/github.rs | |
| parent | 98ec0eb9370bd12225fde1d8c2ff8b8ace693609 (diff) | |
| download | reflectub-85df39e199fa146e22d9cf8ccd635277fe066d12.tar.bz2 | |
main::update(): Change HEAD branch if default branch changed
If the default branch on GitHub changed, change the local mirror's HEAD
to match the new default.
Need to store the default branch in the database now so we can find out
whether it changed.
Diffstat (limited to 'src/github.rs')
0 files changed, 0 insertions, 0 deletions