From 45b3277ca4c41a723a90df17518aed7c991743bf Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 10 Nov 1998 16:52:09 +0000
Subject: Removed references of proof-shell-noise-regexp

---
 todo | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'todo')

diff --git a/todo b/todo
index c7b55385..8638131c 100644
--- a/todo
+++ b/todo
@@ -87,9 +87,8 @@ B da: goal-hyp: this should be more generic.  At the moment, there are
   default behaviour for proof-goal-hyp-fn a hook function.
   That will work for Isabelle too.   (15 mins)
 
-B proof-shell-noise-regexp: seems unused at present, but set
-  in the specific directories.  Either use it or be rid of it!
-  (tms, apparently is used in LEGO mode but should be generic?)
+D Add support to filter out unwanted noise from the prover by setting
+  up a regular expression  proof-shell-noise-regexp (1h)
 
 A Check that byte compilation (and compiled code!) 
   works for both varieties of Emacs. 
-- 
cgit v1.2.3