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 terminator. 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 settings. 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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
