diff options
| author | Pierre Courtieu | 2015-03-03 09:36:22 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2015-03-03 09:36:22 +0000 |
| commit | 3c071eb4457c077286049f03d0bc8f025d497281 (patch) | |
| tree | b35c7790c4f56a5286607c9bbee7ede1bc9621dd /CHANGES | |
| parent | 17185897996db7c001b9c5c1e0cbef8860388e07 (diff) | |
Coqtop always restarted when switching script buffer.
This comes from Hendrik's compile mode and is actually needed even
when this mode is off. When switching scripting buffer, restart the
coq shell process, so that it applies local coqtop options.
Diffstat (limited to 'CHANGES')
0 files changed, 0 insertions, 0 deletions