diff options
| author | Emilio Jesus Gallego Arias | 2017-09-26 00:57:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-09-27 18:13:20 +0200 |
| commit | ec59306708f9aec04ab82a7e03807017e1924507 (patch) | |
| tree | a3b4389c365def2f85eaabc66e1f08d82c516d66 /dev/ci/ci-basic-overlay.sh | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
[stm] Warn about costly Undo operations in batch mode [BZ#5677]
Undo & friends is very expensive in batch mode as backtracking state
is not kept and thus should be recomputed.
We thus warn the user.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions