On 2024-09-11 We 8:34 AM, Robert Haas wrote:
On Mon, Sep 9, 2024 at 3:54 PM Andrew Dunstan <and...@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
