diff options
| author | Jason Gross | 2019-12-18 20:39:06 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-12-19 09:13:20 -0500 |
| commit | baab1c01b22d754df64a09be436d350663cc1c28 (patch) | |
| tree | ea36da8ff129456033af7f62d209b9ee26f3d110 /dev/base_include | |
| parent | 6b309b4297f28fcc6774ac3a19ab830713ec5e62 (diff) | |
Better error reporting when res is not what is expected
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions