Pierre Courtieu <pierre.court...@cnam.fr> writes:

   Since double hit terminator is more or less an alternative to electric
   terminator, I have put them side by side in coq menu, to see if people

OK, I thought "double hit" would modify the behavior of electric

   like it, but I did not make it geenric yet. Maybe one entry for both
   settings with a 3-value setting would be better? 

>From the user perspective this would certainly be better. But if
the implementation is not trivial, we can also keep the two

   Actually tooltips are so useless and annoying (flickering) in coq mode
   that I wanted the disabling option to be as immediate as possible. It
   would probably be better to disable it by default and put the option
   in the settings menu.

Fine with me.

   By the way is there a "emacs gui recommendations somewhere?"

I don't know any. BTW, I just wanted to ask. I don't really have
a strong opinion where those items should go.


ProofGeneral-devel mailing list

Reply via email to