How to fix github-tools when it doesn’t update the docs

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

Remove it and recreate it.