Wladimir J. van der Laan
devtools: make github-merge.py use py3
This makes github-merge.py the first developer tool to go all Python 3 (for context see #7717). The changes are straightforward as the script already was `from __future__ import division,print_function,unicode_literals`. However urllib2 changed name, and json will only accept unicode data not bytes. This retains py2 compatibility for now: not strictly necessary as it's not used by the build system - but it was easy.
|vor 5 Jahren|
|devtools||vor 4 Jahren|
|verify-commits||vor 4 Jahren|
|README.md||vor 4 Jahren|
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.
Tool to verify that every merge commit was signed by a developer using the above