diff options
author | 2017-09-07 11:43:37 +0200 | |
---|---|---|
committer | 2017-09-07 11:43:37 +0200 | |
commit | cb2d69efa4d012a6828077675aba1d2a51d710ef (patch) | |
tree | dfb3ce309af364daa9aa60d58e4a89936b866f4f /theories | |
parent | 70333c957d42d3da208f442d8e7bed7133b57e5c (diff) |
Trying to properly propagate errors in Windows CI script.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions