diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-10-18 08:29:37 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-18 08:29:37 +0200 |
| commit | 9bead2e06fa2866f7fb7cea8eefb6a4fd3225b23 (patch) | |
| tree | c9eeb0de212d265db1be96650f29970d6c28cc01 /servers | |
| parent | bac99b6811bc1215c3bcadb2b5fe8174915932c2 (diff) | |
| parent | fb63ee52fbbc62ab3f1a08ede1f2bd05bfc01db5 (diff) | |
Merge pull request #12208 from neikeq/l
Mono: Fix build with tools=no or target=release
Diffstat (limited to 'servers')
0 files changed, 0 insertions, 0 deletions