id summary reporter owner description type status priority milestone component resolution keywords cc 397 Coq PG: changing scripting buffer and automatically restarting misses first command tews David Aspinall "The issue is that after changing the active scripting buffer, the first assert operation is lost, because the prover is not running. To reproduce go to ``coq/ex/test-cases/multiple-files-single-dir`` and do some scripting in, say, a.v. Then change to a different file (eg b.v) and do some scripting there. To clearly see the effect, make sure the second file (b.v) does not start with a comment. There is a patch in http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000114.html but it needs reviewing. " defect closed major PG-Emacs-4.1 2:pg-emacs fixed