diff options
| author | Thomas Kleymann | 1998-10-05 10:19:47 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-10-05 10:19:47 +0000 |
| commit | e8c5ac4646d162f82465193617885849c1c11969 (patch) | |
| tree | df339a8b1d9bd8874a4d2ee97f8ecd2c708f1748 | |
| parent | a0840203d8579b8448861761c3a67dacea18cc3d (diff) | |
da> BTW, the menus have disappeared!
They are back courtesy of reintroducing an easy-menu-add call.
| -rw-r--r-- | generic/proof.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof.el b/generic/proof.el index ba095928..a0354cf9 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -2090,7 +2090,7 @@ finish setup which depends on specific proof assistant configuration." ;; calculate some strings and regexps for searching (setq proof-terminal-string (char-to-string proof-terminal-char)) - ;; FIXME da: surely these are LEGO (Coq?) specific! + ;; FIXME: these are LEGO specific! (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) @@ -2143,6 +2143,7 @@ finish setup which depends on specific proof assistant configuration." proof-mode-map "Menu used in Proof General scripting mode." (cons proof-mode-name (cdr proof-menu))) + (easy-menu-add proof-mode-menu proof-mode-map) ;; For fontlock ;; FIXME (da): zap commas support is too specific, should be enabled |