diff options
| author | David Aspinall | 2010-10-01 15:38:28 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-10-01 15:38:28 +0000 |
| commit | 0bb355a0ed7db7130758a5e9685ee61ede255c2a (patch) | |
| tree | 65403c6f93b9afb6dc50c1b183d5e88841c50970 /etc | |
| parent | dfff8b899a1aec4236368da71cca2e590c7f03e0 (diff) | |
Add explicit 'invisible flag on the action list for invisible commands.
This means that certain display actions will always be avoided for non-scripting
commands (i.e., hints, anything in `proof-shell-error-or-interrupt-hook').
Diffstat (limited to 'etc')
0 files changed, 0 insertions, 0 deletions