3 Jul
2023
3 Jul
'23
5:56 p.m.
On Mon Jul 3 09:42:22 2023 +0000, Rémi Bernon wrote:
You don't have to, and should not commit configure changes (for reasons like here, this is an unrelated change).
Sorry, after having to rerun configure after every rebase I figured it'd make things easier to just check it in.