From 176c2ea7966af858cd501b88762fbed378f00698 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 15 Apr 2004 13:31:36 +0000
Subject: Updated.

---
 BUGS | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'BUGS')

diff --git a/BUGS b/BUGS
index 505533e8..3008e61a 100644
--- a/BUGS
+++ b/BUGS
@@ -15,6 +15,12 @@ versions, and those which only apply to particular versions.
 
 * Generic problems, for all Emacs versions
 
+** X-Symbol support removed from "secondary" provers (HOL, ACL2, LEGO, Twelf)
+
+If anyone was actually using this, please let me know.  It should be
+very easy to revive by copying coq/x-symbol-coq.el (although a generic
+version might be desirable).
+
 ** Visibility control doesn't distinguish theorems with same name.
 
 If you have more than one theorem with the same name in a buffer,
-- 
cgit v1.2.3