Note to memory: when github-tools explodes and doesn’t work anymore, just double check the submodule in .gitsubmodule.

Remove it and recreate it.