diff options
| author | David Aspinall | 2000-03-22 12:42:17 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-03-22 12:42:17 +0000 |
| commit | fb3c7ce71de3cd1065e00d04ab385be02fb97be2 (patch) | |
| tree | 439292a470f59b1d9da7a5c6b3396a6d8bb716f3 | |
| parent | 9f87e6dff68935c451342f9e98ae679ba310fd48 (diff) | |
Mention %e in doc for proof-shell-cd-cmd.
| -rw-r--r-- | generic/proof-config.el | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index aecdf09a..375674fc 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1145,8 +1145,10 @@ need to bump up this value." "Command to the proof assistant to change the working directory. The format character %s is replaced with the directory, and the proof-terminal-char is added on to the end. +The format character %e is replaced by the directory, after applying +escapes specified in `proof-shell-string-escapes', which see. -This is used to define the function proof-cd which +This setting is used to define the function proof-cd which changes to the value of (default-directory) for script buffers. For files, the value of (default-directory) is simply the directory the file resides in. |