Follow-up Comment #3, sr #111372 (group administration): [comment #2 comment #2:] > What I would like to do is to delete the "master" branch and rename another > branch, namely "new_parser_a", to "master" or "main" or something like that.
I've reset master to new_parser_a; typical commands for the remote users to
update are 'git fetch origin' and 'git reset --hard origin/master'; please let
me know if they don't work for you.
> I don't think it would be worth changing the name of the project just to have
> access to the web interface for administering the repository.
No, of course not; I'll fix the Web UI instead.
_______________________________________________________
Reply to this item at:
<https://savannah.gnu.org/support/?111372>
_______________________________________________
Message sent via Savannah
https://savannah.gnu.org/
signature.asc
Description: PGP signature
