Scheduled service maintenance on November 22
On Friday, November 22, 2024, between 06:00 CET and 18:00 CET, GIN services will undergo planned maintenance. Extended service interruptions should be expected. We will try to keep downtimes to a minimum, but recommend that users avoid critical tasks, large data uploads, or DOI requests during this time.
We apologize for any inconvenience.
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.