From 8c84cda43b393f0f4264df25a8aec91ea5f94b53 Mon Sep 17 00:00:00 2001
From: Paul Callaghan
Date: Thu, 11 Nov 1999 16:16:58 +0000
Subject: small changes to plastic mode

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

(limited to 'generic')

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 2b948fa2..44ef4e5e 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1057,8 +1057,7 @@ particularly in proof-start-queue and proof-shell-exec-loop."
     ;; Lego uses this hook for setting the pretty printer
     ;; width, Coq uses it for sending an initialization string
     ;; (although it could presumably use proof-shell-init-cmd?).
-    ;; Paul Callaghan wants to use this hook to massage STRING
-    ;; to remove literate-style markup from input. 
+    ;; Plastic uses this hook to remove literate-style markup from 'string'. 
     (run-hooks 'proof-shell-insert-hook)
 
     ;; Now we replace CRs from string with spaces. This was done in
@@ -1778,4 +1777,4 @@ processing."
 
 
 (provide 'proof-shell)
-;; proof-shell.el ends here.
\ No newline at end of file
+;; proof-shell.el ends here.
-- 
cgit v1.2.3