From a4b24e4e30d10a79f3d8fc90d1acd69b80b4c2ab Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 7 Dec 2006 19:51:33 +0000
Subject: proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup,
 which breaks Poly/MK 5;

---
 generic/proof-config.el | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'generic')

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)
 
-- 
cgit v1.2.3