aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--coq/coq-unicode-tokens.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index 124a0146..d02ea70b 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -172,7 +172,7 @@ results will be undefined when files are saved."
("-O" . "⊖")
("xO" . "⊗")
("/O" . "⊘")
- (".O" . "⊙")
+ ;(".O" . "⊙") ; bad interaction with electric terminatore and double hit terminator
("|+" . "†")
("|++" . "‡")
("<=" . "≤")