On 2024-09-11 We 8:34 AM, Robert Haas wrote:
> On Mon, Sep 9, 2024 at 3:54 PM Andrew Dunstan <andrew@dunslane.net> wrote:
>> There are some serious obstacles to changing it all over, though. I
>> don't want to rewrite all the history, for example.
> Because of the way git works, that really wouldn't be an issue. We'd
> just push the tip of the master branch to main and then start
> committing to main and delete master. The history wouldn't change at
> all, because in git, a branch is really just a movable pointer to a
> commit. The commits themselves don't know that they're part of a
> branch.
>
> A lot of things would break, naturally. We'd still all have master
> branches in our local repositories and somebody might accidentally try
> to push one of those branches back to the upstream repository and the
> buildfarm and lots of other tooling would get confused and it would
> all be a mess for a while, but the history itself would not change.
I think you misunderstood me. I wasn't referring to the git history, but
the buildfarm history.
Anyway, I think what I have done should suffice. You should no longer
see the name HEAD on the buildfarm server, although it will continue to
exists in the database.
Incidentally, I wrote a blog post about changing the client default name
some years ago:
<http://adpgtech.blogspot.com/2021/06/buildfarm-adopts-modern-git-naming.html>
I also have scripting to do the git server changes (basically to set its
default branch), although it's rather github-specific.
cheers
andrew
--
Andrew Dunstan
EDB: https://www.enterprisedb.com
