On Fri, Jun 19, 2020 at 10:07 AM Geert Uytterhoeven <[email protected]> wrote: > > Indeed. It looks like this whole list is completely unsorted, and was created > by appending new definitions at the bottom.
The "historical ordering" :) +1 for sorting, whatever the ordering (and perhaps adding a comment saying which one it is). Cheers, Miguel
