On Wed, Aug 7, 2024 at 9:01 PM Robert Haas <robertmh...@gmail.com> wrote: > 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.
Correct, but something looks better than nothing. > 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. +1 ------ Regards, Alexander Korotkov Supabase