David Aspinall <david.aspin...@ed.ac.uk> writes:
So, yes, you may need to adjust the load path manually with
the scriting activate/deactivate hooks.
Undoing those Add LoadPath commands with Remove LoadPath commands
would be rather difficult. If one adds a directory which is
already in the LoadPath, coq reorders the LoadPath, a subsequent
remove will not yield the starting state.
proof-shell-invisible-command is designed for sending
diagnostic and control commands which are not scripting
OK, is there an alternative that I could use from inside
proof-activate-scripting-hook in order to get undo behaviour?
ProofGeneral-devel mailing list