> I believe setting cursor-in-non-selected-windows to nil (and
> leaving cursor-type unchanged) in *goals* and *response* would be
> more appropriate.

You might like to check the VCS to see what is the history of that code,
but I suspect that those cursor-type settings came before
cursor-in-non-selected-windows was available.
In any case I completely agree (and I seem to remember adding
cursor-in-non-selected-windows settings myself already).

ProofGeneral-devel mailing list

Reply via email to