From 9b5441aa6e3b1690afd98e84e55f2faaab4f1f0d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 25 Jan 2008 15:48:02 +0000
Subject: Remove unicode tokens from menu, this is experimental.

---
 generic/proof-menu.el | 1 +
 1 file changed, 1 insertion(+)

diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 39717c85..65368192 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -342,6 +342,7 @@ without adjusting window layout."
 ;;       :selected (and (boundp 'x-symbol-mode) x-symbol-mode
 ;; 		     x-symbol-use-unicode)]
 
+;; Experimental:
 ;;      ["Unicode Tokens" (proof-unicode-tokens-toggle 
 ;; 			(if unicode-tokens-mode 0 1))
 ;;       :active (proof-unicode-tokens-support-available)
-- 
cgit v1.2.3