The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

I apologize for the triviality of this question, but I've just spent
an hour reading manuals and the rest of the Internet. I can't be the
only one trying to accomplish this.

I am on Emacs 25.3 with the latest Proof-general from Homebrew (4.4_2 it 
seems).

I have to monitors and would like to place the *goal* and *response*
buffers into separate windows on the second display. This is doable by
setting

* proof-three-window-enable to t
* proof-multiple-frames-enable to t
* proof-delete-empty-windows to nil

I can manually position the *response* and *goal* frames where I want
them to be.

The problem is this: every time I kill Coq with C-c C-x, or I just
switch to a new buffer and start a new coq session, Proof General
moves the two frames back to the first display, on top of my existing
Emacs buffer.

Is there a way to tell Emacs to bloody leave the frames alone? I don't
know of any other application with the audacity to move windows around
without explicit user constent.

The ideal solution would be to tell Emacs where specifically and of
what size the two frames from *response* and *goal* should be.

With kind regards,

Andrej