diff options
author | Rémi Verschelde <rverschelde@gmail.com> | 2021-02-05 12:07:40 +0100 |
---|---|---|
committer | Rémi Verschelde <rverschelde@gmail.com> | 2021-02-05 12:07:40 +0100 |
commit | d6404fd7a07f4828b4e437a579d4d9638a651d5a (patch) | |
tree | 3c7ba1ae28e4008690bd9e804bae37a20886d3c0 /editor | |
parent | 3de411cb836cf13c41bb4b048dd5af5ab52a077c (diff) |
CI: Build Linux editor without Mono, sanitizers with Mono
The Mono builds are with mono_glue=no so they're not usable,
and it would be convenient if the main tools=yes target=release_debug
artifacts could actually be used.
Diffstat (limited to 'editor')
0 files changed, 0 insertions, 0 deletions