I wrote:

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

I've committed this change yesterday. 

David, quite some changes accumulated since Release-4-2pre120430. 
Do you think you can schedule another prerelease this or next

Stefan Monnier <monn...@iro.umontreal.ca> writes:

   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

Well, if the :version tag is right,
cursor-in-non-selected-windows exists since version 21.1 from
2001. The cursor-type change was first committed 2008.

BTW, can you explain, way cursor-in-non-selected-windows is
customizable while cursor-type is not?


ProofGeneral-devel mailing list

Reply via email to