diff options
| author | David Aspinall | 2010-10-01 15:07:07 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-10-01 15:07:07 +0000 |
| commit | 1604db92ae0d21b58caafb481aef73570056a122 (patch) | |
| tree | d97fd823c24b0eb2a1dce8612fc19335f58f67af /etc | |
| parent | 7649ff839e9ee7ddbb41b53c30a96c5fbf8316d8 (diff) | |
proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting input (no non-nil flags in queue)
Diffstat (limited to 'etc')
0 files changed, 0 insertions, 0 deletions