In November 2023, we merged several repositories to this one, maintaining the commit history. These repositories were then archived.

It would have been better to save un-merged commits all at once, by giving the commits branch names and then merging them all at once. However, we failed to do this, and instead merged them one at a time.