Re: Change branch name in GitHub #project #communication

Matteo Lissandrini (AAU)

Hi Tomas,

I think I can reassure you on practical issues:

1) so Github is already working on this:

2) the rename is maybe an issue for existing local branches/forks/clones with active changes, which I would guess are at best a handful.

3) when we create a new repo on github, creating the appropriate branch and delete master is probably a matter of five minutes?

Instructions to change the default branch exist already:

a) On github:

b) On local&github:

c) automatically on new repos:


Matteo Lissandrini

Department of Computer Science
Aalborg University

From: <> on behalf of tomas Navarrete via <>
Sent: 17 June 2020 17:07:20
Subject: Re: [bonsai] Change branch name in GitHub #communication #project

Dear All,

I totally understand the reason behind the wish to change names.
Now, beware that:

The default branch name in Git is master.<>

so, every time we create a new repo, or initialize one, we'll need to update this behavior (MAYBE until github does something about it ... which is funny, because they kind of have a dominating position in the "free git hosting" namespace ;) )

For very practical reasons, I would stand against renaming existing repositories and only apply a name change on newly created ones, and loudly anounce this in the README of the repo.
If this (default branch name) is configurable, then we should look to implement a name that is fine with us.


Join to automatically receive all group messages.