Closed edkerk closed 3 years ago
It should be possible to just change the target branch in this PR without opening a new one?
Also, is the intention to resolve #11 as part of this release, or would it be better to postpone it?
I didn't close it manually, but I did just change the name of devel
to develop
, in accordance with #258. It might be that GitHub is at the moment still processing the name change, and will reopen it soon again to the newly named branch.
Re #11, this would take longer to resolve, so probably good to postpone to distribute as 2.5.1?
Oh, interesting side-effect of branch renaming. Sure, it's okay reserve #11 for a subsequent release.
~Here is mentioned:~
~After the rename is complete, GitHub provides instructions on the repository's home page directing contributors to update their local Git environments.~
~Considering this is not showing on the home page yet, I assume they haven't finished the procedure yet. If this is not resolved by tomorrow I'll manually fix this PR.~
This seems to be referring to changing name of the default branch, not other branches. Because the "from" branch is renamed, the source is missing and seems like I'll have to remake the PR. Now done as #262.
Main improvements in this PR:
rxnMiriams
orrxnKEGGpathways
) (PR #253)standard-GEM
specifications (PR #257)master
anddevel
branches tomain
anddevelop
(PR #261)Also rename your local branches to
main
anddevelop
:PR #261 should first be merged
I hereby confirm that I have:
main
as a target branch (top left drop-down menu)