diff options
| author | Gaëtan Gilbert | 2018-10-15 14:03:06 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-15 10:27:34 +0100 |
| commit | b7203d14aad300c0ef02f66516ce0595182c81cd (patch) | |
| tree | f3b147f9c5141560e32bb252dbf0c05fbdb7af27 /dev/ci/ci-plugin-tutorial.sh | |
| parent | b6f65c72cce697d7acc11f731983a8c18f497d10 (diff) | |
Make set_typing_flags "smart"
Fix #8609
gares said: I believe it was introduced in de20a45 where the
option (part of the summary) is moved to the save env. By setting the
summary, you unshare the safe env. Now we do that only if needed. The
stm uses `==` on the safe env to detect tactics that alter the env, eg
abstract.
Diffstat (limited to 'dev/ci/ci-plugin-tutorial.sh')
0 files changed, 0 insertions, 0 deletions