aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol98
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-22 12:53:35 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-22 12:53:35 +0000
commitaaf47bf358301b0f09e3500ea9eb3f596b7ee7c5 (patch)
tree5ea75c26e20695c30d645e05dd2a9f45bbf44bff /hol98
parent62acb71bcf74d7a8123bf65fb9855815fd3acba3 (diff)
Use new format character %s to %e to cope with nasty filenames with backslashes.
Diffstat (limited to 'hol98')
-rw-r--r--hol98/hol98.el2
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