| Patch | Description | Author | Forwarded | Bugs | Origin | Last update |
|---|---|---|---|---|---|---|
| restrict-installed-provers.patch | restrict the installed provers to Coq only IMHO it does not make sense to install provers that are incomplete, obsolete or broken or that had their last release in 1998. It does not make sense to install Isar or Isabelle, because Isabelle is always distributed with its own copy of Proof General. This leaves us with just two installed provers. |
Hendrik Tews <hendrik@askra.de> | no | |||
| dont-install-mmm-mode.patch | don't install contrib/mmm mmm-mode is available as package and added to the dependencies | Hendrik Tews <hendrik@askra.de> | no | |||
| fix-package-name-in-install-path.patch | use proofgeneral as subdir in various install directories | Hendrik Tews <hendrik@askra.de> | no | |||
| dont-install-elc.patch | don't put elc files into the package | Hendrik Tews <hendrik@askra.de> | no | |||
| only-install-simplified-pg-script | don't install upstream scripts There are different reasons for not installing the different scripts, but in the end only coqtags remains. . Scripts for Isar or Lego are obviously not installed. . The proofgeneral starting script is replaced with our own simplified version, which is the only script installed. |
Hendrik Tews <hendrik@askra.de> | no | |||
| debian-specific-site-init.patch | use a debian specific emacs site init file | Hendrik Tews <hendrik@askra.de> | no | |||
| prepare-user-manual | install the user manual This patch builds the info, html and pdf version of the user manual with some Debian specific changes. They are also moved/renamed to fit Debian's conventions. The PG-adapting manual is not included in any package. |
Hendrik Tews <hendrik@askra.de> | no | |||
| install-examples.patch | install example files in /usr/share/doc | Hendrik Tews <hendrik@askra.de> | no | |||
| transition_to_makeinfo.patch | use makeinfo, instead of obsolete texi2html | Hideki Yamane <henrich@debian.org> | no | 2014-02-15 | ||
| fix-coqtags.patch | fix perl syntax errors in coqtags | Hendrik Tews <hendrik@askra.de> | no | |||
| desktop-keyword-entry.patch | add Keywords field to desktop file to make lintian happy and disable StartupWMClass to let gnome show the emacs icon | Hendrik Tews <hendrik@askra.de> | no |