:-) Good point, (define-key coq-mode-map (kbd ".") 'self-insert-command) (define-key coq-mode-map (kbd ";") 'self-insert-command)
Should do the thing but I will add a customization variable. Sorry for the inconvenience, I did not think someone would notice this before I finish my experiment on that. My curiosity: did it jump at you by accident? Hitting ".." quickly is not so common is it? Regards, P. 2012/9/3 Hendrik Tews <t...@os.inf.tu-dresden.de>: > Hi, > > coming back from holiday, I got the new double hit terminator > feature on checkout. Being not open-minded about new things, I > wanted to disable it. But how to do that? > > Bye, > > Hendrik > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
