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