On Wed, Aug 7, 2024 at 1:15 PM Nathan Bossart <nathandboss...@gmail.com> wrote: > > We could use git notes. The UI is a bit inconvenient (they have to be > > pushed and pulled separately from commits), but they seem useful enough. > > Yeah, I spend a lot of time on commit messages because they're pretty much > written in stone once pushed. I'd definitely use git notes to add errata, > follow-up commits that fixed/reverted things, etc.
I think this could be a good idea, although it wouldn't really fix the problem, because in the case of both this commit and the one I mentioned earlier today, all you could do with the note is point out the earlier mistake. You couldn't actually fix it. Also, for the notes to be useful, we'd probably need some conventions about how we, as a project, want to use them. If everyone does something different, the result isn't likely to be all that great. -- Robert Haas EDB: http://www.enterprisedb.com
