Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?

2011-01-14 Thread Hendrik Tews
David Aspinall david.aspin...@ed.ac.uk writes: I suggest refactoring the setting of prog-command-line in proof-shell-start into a new function which does this, so (proof-shell-prog-command-line) returns the command line you want. That would clear up the beginning of proof-shell-start

Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?

2011-01-14 Thread David Aspinall
This is, however, not the expected simplification. I decided for this simple change, because it keeps the functionality of other proof assistants without that I have to touch their code. This sounds wise, and what Pierre originally suggested, although if I've followed it seems as if that's