aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-07 19:15:10 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-07 19:16:26 +0100
commit1222bc9e677c14884dd7c0f475003f01eb5fb1b1 (patch)
tree17dd07f8556426d1d5289a01a630f3fd125314b9 /stm
parent47e43e229ab02a4dedc2405fed3960a4bf476b58 (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 'stm')
0 files changed, 0 insertions, 0 deletions