> 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).


        Stefan
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to