Closed sloede closed 3 years ago
Merging #15 (a7778a2) into master (02248fa) will not change coverage. The diff coverage is
n/a
.
@@ Coverage Diff @@
## master #15 +/- ##
=======================================
Coverage 57.12% 57.12%
=======================================
Files 65 65
Lines 9470 9470
=======================================
Hits 5410 5410
Misses 4060 4060
Flag | Coverage Δ | |
---|---|---|
unittests | 57.12% <ø> (ø) |
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
Legend - Click here to learn more
Δ = absolute <relative> (impact)
,ø = not affected
,? = missing data
Powered by Codecov. Last update 02248fa...a7778a2. Read the comment docs.
I se no reason why not, but does this affect PR14?
Now that #14 is already merged, this question is moot, but no, it wouldn't have affected it. GitHub automatically redirects all PRs to the new default branch.
In keeping with the wider GitHub and code development community, I propose to rename the default branch from
master
tomain
, as we have done for virtually all other repositories. While on the surface it seems to be a political question, the overwhelming trend is moving tomain
: new repos on GitHub usemain
by default, andgit
itself has implemented the ability to change the default branch (see more details here). Thus I also think it makes sense from the "principle of least astonishment" for other users.For new users, this change is transparent, since when they clone from GitHub they will automatically check out
main
instead ofmaster
. For existing users, it is a two-liner to renamemaster
tomain
in pre-existing local clones. However, not renaming anything will work just as well, since GitHub internally forwards all references tomaster
tomain
.Note: Please do not merge this until the actual name change has been applied to the GitHub repo.