diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2000-03-22 12:53:35 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-22 12:53:35 +0000 |
commit | aaf47bf358301b0f09e3500ea9eb3f596b7ee7c5 (patch) | |
tree | 5ea75c26e20695c30d645e05dd2a9f45bbf44bff /hol98 | |
parent | 62acb71bcf74d7a8123bf65fb9855815fd3acba3 (diff) |
Use new format character %s to %e to cope with nasty filenames with backslashes.
Diffstat (limited to 'hol98')
-rw-r--r-- | hol98/hol98.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/hol98/hol98.el b/hol98/hol98.el index 41f2f484..efb22a55 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -31,7 +31,7 @@ proof-showproof-command "p()" proof-undo-n-times-cmd "(pg_repeat backup %s; p());" proof-auto-multiple-files t - proof-shell-cd-cmd "FileSys.chDir \"%s\"" + proof-shell-cd-cmd "FileSys.chDir \"%e\"" proof-shell-prompt-pattern "^[->] " proof-shell-interrupt-regexp "Interrupted" proof-shell-start-goals-regexp |