diff options
| author | Enrico Tassi | 2020-05-18 18:33:09 +0200 |
|---|---|---|
| committer | GitHub | 2020-05-18 18:33:09 +0200 |
| commit | ffe1de0bab363902f3e9c517345713f74cfa3071 (patch) | |
| tree | 4cf516bf3ce5c63479139dbc20014ffd5ed83322 /dev/tools/github-check-prs.py | |
| parent | e1e4073f551c34cbaf5b510c3e2eaa11df8b095a (diff) | |
Update release-process.md
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions