Re: 2 coq emacs modes

[David MENTRE <dmentre@linux-france.org>]

Hello,

2012/1/13 Hendrik Tews <tews@os.inf.tu-dresden.de>:
> 1) leave the situation as is
>  People not using Proof General will hopefully not install Proof
>  General and therefore don't see the problem.
>
> 2) make a separate package for the emacs mode in Coq
>  This way users are forced to make a decision. However, it is
>  questionable if this is worth the effort, because nobody seems
>  to use the coq-mode distributed with coq. coq-mode from
>  Coq was completely broken in squeeze (#605024) and only people
>  using Proof General noticed it, i.e., people either install coq
>  allone and do not use emacs _or_ they install coq and Proof
>  General.
>
> 3) delete coq-mode from package coq
>
> 4) ask a debconf question when Proof General is installed

Another proposal:

  5) Still install coq-mode but request a user action (i.e. putting
something in .emacs) to activate it. Document it in README.Debian.

Best regards,
d.