diff options
| author | w0rp <w0rp@users.noreply.github.com> | 2018-01-12 12:09:30 +0000 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-12 12:09:30 +0000 |
| commit | 5005871644e102120eee922718379cd992dfbfdf (patch) | |
| tree | a957a60a4547e6ab99f763bf12d8ed868710870f /doc | |
| parent | 65fa901ef0c15a2cd8c17642b0c5f0108ed93585 (diff) | |
| parent | 68d4a2216ca8edb7396f88352cfe807fa771ca7e (diff) | |
| download | ale-5005871644e102120eee922718379cd992dfbfdf.zip | |
Merge pull request #1256 from jonatanolofsson/master
Fix #1255: Move extra clang-check args to before user options
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions