diff options
| author | Maxime Dénès | 2018-03-26 18:20:24 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-26 18:20:24 +0200 |
| commit | 01b7de3a673eb89cea61442c4db721aad9520c9f (patch) | |
| tree | a5322ed7abf69902f97c720c9c3839d33fc071d1 /dev/tools/github-check-prs.py | |
| parent | c1dcb97cf95c10d19f67689108da8726232da4fb (diff) | |
| parent | 689b19c5ff764697f3ac39261576444ca2431c73 (diff) | |
Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes AppVeyor fail.
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions