diff options
| author | Emilio Jesus Gallego Arias | 2017-12-01 20:29:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-04 12:21:38 +0100 |
| commit | 195a652e38bcb6f58c156495492999ea8ee4e64e (patch) | |
| tree | 19788da699483c51d3560feb435fbec880d85911 /dev/doc | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
[vernac] Couple of tweaks missing from previous PRs.
In particular we must invalidate the state cache in the case of an
exception.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions