diff options
| author | Maxime Dénès | 2018-05-29 21:59:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-29 21:59:45 +0200 |
| commit | b073a2ceebe1d332d27852b6504cd809d21613b8 (patch) | |
| tree | b7671cf72ede2462629e050738ff8c1fd117f0a1 /dev/tools/github-check-prs.py | |
| parent | ec598cca8ba337534ef58fd9bf62328bea62cb17 (diff) | |
| parent | 07aa836ac323bb0898e063d0e54f29e456dac809 (diff) | |
Merge PR #7566: Remove a dead old-refman file.
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions