|
|
@@ -3,7 +3,7 @@ Repository Tools |
|
|
|
|
|
|
|
### [Developer tools](/contrib/devtools) ### |
|
|
|
Specific tools for developers working on this repository. |
|
|
|
Contains the script `github-merge.sh` for merging github pull requests securely and signing them using GPG. |
|
|
|
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.sh` script. |
|
|
|
Tool to verify that every merge commit was signed by a developer using the above `github-merge.py` script. |