aboutsummaryrefslogtreecommitdiff
path: root/plastic
diff options
context:
space:
mode:
authorDavid Aspinall2009-09-06 12:08:56 +0000
committerDavid Aspinall2009-09-06 12:08:56 +0000
commit46aebf7c30b09a7371f9dbbf2f4b7e1505429a38 (patch)
tree442f6df9ff5351bc06ac739e2d083b4b0248cc9f /plastic
parent9e6fe41dcf92a91cfc4b1f6da2f3cfa0a9b62716 (diff)
Remove proof-shell-wakeup-char
Diffstat (limited to 'plastic')
-rw-r--r--plastic/plastic.el2
1 files changed, 0 insertions, 2 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el
index a6939f41..7707ee56 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -463,8 +463,6 @@ We assume that module identifiers coincide with file names."
proof-shell-assumption-regexp plastic-id
proof-shell-goal-regexp plastic-goal-regexp
pg-subterm-first-special-char ?\360
- proof-shell-wakeup-char ?\371 ;; only for first send?
-;; proof-shell-wakeup-char nil ;; NIL turns off annotations.
pg-subterm-start-char ?\372
pg-subterm-sep-char ?\373
pg-subterm-end-char ?\374