diff options
| author | David Aspinall | 1998-11-25 12:46:53 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-25 12:46:53 +0000 |
| commit | 50035e0a85a8d3adfaad4689049cffd25fef9dfa (patch) | |
| tree | 01caf30a60d2d0475b11b75d06c907c69cbbfd0a /doc/dir | |
| parent | d37b534a1d29315488b04e066701fe7188550781 (diff) | |
Improved error handling in proof-deactivate-scripting since
it's used in a kill hook.
Diffstat (limited to 'doc/dir')
0 files changed, 0 insertions, 0 deletions