diff options
| author | David Aspinall | 2000-03-09 09:27:07 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-03-09 09:27:07 +0000 |
| commit | 21b3bfdb08081ac10a59c9bc61c90ea85c7e940e (patch) | |
| tree | 617992f8a6ebba14fff210fd7c0ab7a23f92b8f4 /generic/proof-config.el | |
| parent | ae7c256d964dd24b2d066d5d5da2da762c843aca (diff) | |
Added proof-shell-process-connection-type.
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 37e5ad27..9860434e 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1410,6 +1410,21 @@ to do syntax highlighting with font-lock." ;; 5c. hooks and hook-related variables ;; +(defcustom proof-shell-process-connection-type + ;; Use ptys unless it seems like we're on Solaris. + (not (string-match "[sS]un" (or (getenv "ARCH") ""))) + "The value of process-connection-type for the proof shell. +Set non-nil for ptys, nil for pipes. +The default (and preferred) option is to use pty communication. +However there is a long-standing backslash/long line problem with +Solaris which gives a mess of ^G characters when some input is sent +which has a \ in the 256th position. We do not force pipes everywhere +because this risks loss of data and some proof assistants do not +flush their output by default after each interaction, which breaks +pipe communication." + :type 'boolean + :group 'proof-shell) + (defcustom proof-shell-insert-hook nil "Hooks run by proof-shell-insert before inserting a command. Can be used to configure the proof assistant to the interface in |
