From: Jeff King <peff@peff.net>
Date: Fri, 27 Sep 2024 04:15:16 GMT
Subject: Re: Can a note be pushed to origin?
Message-ID: <20240927041516.GA568026@coredump.intra.peff.net>
In-Reply-To: <6b69af87-9002-46a7-a5f3-3fa1fb7ba9df@app.fastmail.com>

On Wed, Sep 25, 2024 at 05:29:30PM +0200, Kristoffer Haugsbakk wrote:

> That will refuse to update if your own notes ever diverge from the
> remote.  If you want to always overwrite your local notes with the
> remote ones:

There are some specialized strategies for merging notes (e.g., taking
the union of lines). See the "merge" subcommand in git-notes(1).

I don't recall ever really using it myself, and I don't think there's
really any porcelain support, so you're on your own to invoke the merge.
But I guess the use case would be something like:

  # fetch their notes into a holding spot
  git config remote.origin.fetch refs/notes/commits:refs/notes/origin/commits

  # and then after every fetch, you merge if necessary. By default we're
  # merging into our own "refs/notes/commits". And it should be OK to
  # use the short "origin/commits" here, since notes-refs have their own
  # special lookup rules. Though using the fully qualified refname is
  # probably reasonable, too.
  git fetch
  git notes merge -s union origin/commits

-Peff