id,summary,reporter,owner,description,type,status,priority,milestone,component,resolution,keywords,cc 406,auto compile bugs when some outputs is done by coqc,courtieu,coquser,"To reproduce the bug: 1) have in file foo.v the following: Eval compute in 0. 2) Have in file bar.v the following: Require Import foo. 3) then try to script bar.v (with auto-compilation on), compilation of foo.v is started automatically but then there is an error due to the read-only status of coq-compile-response buffer. I think this is due to the fact that coqc compilation *does* the output. Cheers, P. --------------8X---------------- excerpt of buffer *Messages*: Check /home/courtieu/titi.vo Recompile /home/courtieu/titi.v Waiting for process to die...done condition-case: Buffer is read-only: # ",defect,closed,critical,PG-Emacs-4.2,2:pg-emacs,upstream,auto-compilation,tews@…