diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-10-27 15:18:28 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-27 15:18:28 +0000 |
| commit | fc9af819f6faa4214c376f74a14e4db45178c921 (patch) | |
| tree | 6505dc2075ca4fa4cdbab9ed2d2f0e5bff502efb /generic/proof-script.el | |
| parent | 787e3d0cccf840d87111a5626deaeb8c07156a9d (diff) | |
Moved pbp-goal-command and pbp-hyp-command to proof-config.Moved LEGO specifix.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 4447f368..b423aed9 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1428,10 +1428,6 @@ 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: these are LEGO specific! - (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) - (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) - ;; FIXME da: I'm not sure we ought to add spaces here, but if ;; we don't, there would be trouble overloading these settings ;; to also use as regexps for finding comments. |