:-) 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?
2012/9/3 Hendrik Tews <t...@os.inf.tu-dresden.de>:
> 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?
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list