Closed rnestler closed 3 months ago
@benhid What was the reason to close this?
Sorry, @rnestler,
I accidentally deleted the develop branch, and as a result, the pull request was automatically closed.
Reopening PR!
I accidentally deleted the develop branch, and as a result, the pull request was automatically closed.
Alright. Is there a reason to use the develop branch as an intermediate for developing instead of just using the main branch? Since main
is set as the default branch on GitHub this is quite confusing for contributors, since PRs will be opened against main by default.
@benhid What is the status on this?
@benhid What is the status on this?
@ajnebro Care to take a look at this as well?
What is the reason for the duplicated documents? I just fixed the branch name in both of them, but I'm still wondering why.