diff options
| author | Makarius Wenzel | 2006-12-07 19:51:33 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2006-12-07 19:51:33 +0000 |
| commit | a4b24e4e30d10a79f3d8fc90d1acd69b80b4c2ab (patch) | |
| tree | 145672aed12d42374153122d2dafff4b39ef652b /generic | |
| parent | 07559fb1fa3cad5e3fdd2fd5b14313e7ad455c9b (diff) | |
proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup, which breaks Poly/MK 5;
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 0ca0155a..d8261e79 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -2334,11 +2334,9 @@ something in scripting buffer, `save-excursion' and/or `set-buffer'." (defcustom proof-shell-pre-interrupt-hook nil - "Run immediately after `comint-interrupt-subjob' is called. -This hook is added to allow customization for Poly/ML and other -systems where the system queries the user before returning to -the top level. For Poly/ML it can be used to send the string \"f\", -for example." + "Run immediately after `comint-interrupt-subjob' is called. This +hook is added to allow customization for systems that query the user +before returning to the top level." :type '(repeat function) :group 'proof-shell) |