On the gin webinterface a 'delete branch' button is offered after merging a PR. However, using this functionality only deletes the feature branch, but not the corresponding synced branch. Currently this one still needs to be deleted manually via deleting from local: git push -d origin synced/<feature>.
I think it would make sense to include the deletion of the synced branch for the 'delete branch' button.
On the gin webinterface a 'delete branch' button is offered after merging a PR. However, using this functionality only deletes the feature branch, but not the corresponding synced branch. Currently this one still needs to be deleted manually via deleting from local: `git push -d origin synced/<feature>`.
I think it would make sense to include the deletion of the synced branch for the 'delete branch' button.
On the gin webinterface a 'delete branch' button is offered after merging a PR. However, using this functionality only deletes the feature branch, but not the corresponding synced branch. Currently this one still needs to be deleted manually via deleting from local:
git push -d origin synced/<feature>.I think it would make sense to include the deletion of the synced branch for the 'delete branch' button.
That's a good point and an oversight on our part when adding annex support.