Repository Tools --------------------- ### [Developer tools](/contrib/devtools) ### Specific tools for developers working on this repository. Contains the script `github-merge.py` for merging github pull requests securely and signing them using GPG. ### [Verify-Commits](/contrib/verify-commits) ### Tool to verify that every merge commit was signed by a developer using the above `github-merge.py` script.