Hi Mike, I pushed the whole patch series as f30e8f29096e3ae2a4de689690daf5fa27a8c91b! \o/ For the tla2tools patch, I added the patch to gnu/local.mk. I also had to change the hash of the checkout, because I wouldn’t get the same one. There are two possibilities: either upstream changed the tag upstream, or you were looking at a same-named store item actually coming from a different commit. Please take a look and let us know if anything’s amiss. Thanks for this heroic effort, and apologies for the delay! Ludo’.