diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-07 19:15:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-07 19:16:26 +0100 |
| commit | 1222bc9e677c14884dd7c0f475003f01eb5fb1b1 (patch) | |
| tree | 17dd07f8556426d1d5289a01a630f3fd125314b9 /ide | |
| parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) | |
[toplevel] Disable error resiliency in `-quick` mode.
Fixes #6707, indeed, the STM was treating some errors as recoverable
thus `-quick` did succeed too often.
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions