diff options
| author | Healfdene Goguen | 1998-05-12 14:51:27 +0000 |
|---|---|---|
| committer | Healfdene Goguen | 1998-05-12 14:51:27 +0000 |
| commit | 59a36f4cbaa07ca3f037c813ecbf8c0240706359 (patch) | |
| tree | ec170d86814bb4b2d42b4b3973a69563c359ecf7 /script-management.texinfo | |
| parent | 93fd0885cfa1679cc0e7231c0e4d4ebb188e4b05 (diff) | |
Added hook `coq-shell-init-hook', for `proof-shell-insert-hook'.
This initializes undo limit and changes directory to that associated
with buffer.
This is because Coq has a command line option to run with emacs mode.
Diffstat (limited to 'script-management.texinfo')
0 files changed, 0 insertions, 0 deletions