diff options
| author | Emilio Jesus Gallego Arias | 2018-08-20 17:31:22 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-08-20 17:31:22 +0200 |
| commit | b393d91c0f628f0687486fb2d321f262981a4d33 (patch) | |
| tree | 0a54acc53d589e4e06832e051893c984c92edeaa /tools | |
| parent | 8a9c8f66a8c92ceb54e5325418c1a2074a7e4c6c (diff) | |
| parent | 6f0d9565eb67acf7bf8f708ef5a2b1ddabc668a5 (diff) | |
Merge PR #8136: Do not run 32-bit Windows builds on pull requests.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions