diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2018-02-27 11:24:54 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-27 11:24:54 +0100 |
| commit | a6d4438faba3eb23fd526d477c37732ced37047e (patch) | |
| tree | 98762ebc631f44ef0934e78430aacb32c87a81e7 /version.py | |
| parent | 5dfaf89aca2185ff4ef5f960f61e5a26b8245a70 (diff) | |
| parent | 90a705d67102c30083d91cff47f35300eb5049a9 (diff) | |
Merge pull request #17075 from paulloz/fix-build-mono-debug-notools
[mono] fix build error when compiling with mono, tools=no, target=debug
Diffstat (limited to 'version.py')
0 files changed, 0 insertions, 0 deletions