diff options
| -rw-r--r-- | debian/README.Debian | 30 | ||||
| -rw-r--r-- | debian/changelog | 6 |
2 files changed, 9 insertions, 27 deletions
diff --git a/debian/README.Debian b/debian/README.Debian index d91bc559..7da3eb64 100644 --- a/debian/README.Debian +++ b/debian/README.Debian @@ -5,7 +5,7 @@ Binary (in)compatibility ------------------------ The compiled libraries of Coq (the *.vo) are not expected to be backward or -upward compatible between releases (including plX releases). In case of a new +forward compatible between releases (including plX releases). In case of a new upstream release, your Coq files should be recompiled. @@ -13,30 +13,6 @@ Coq frontends ------------- For interactive use of coqtop, we suggest - either the Debian cle package -- or the Proof-General (x)emacs mode, which unfortunately can not be -distributed by Debian for copyright reasons. However, a Debian package -might become available at proof general home page in the future -(http://zermelo.dcs.ed.ac.uk/~proofgen) +- or the Proof-General (x)emacs mode -However we recommand you to use the CoqIde gtk interface provided in coqide. - - -Unstripped binaries -------------------- - -Note that all bytecode files in this package need to be left -'unstripped' after compiling. The reason is the following: - - It is possible to strip the .out corresponding to ocaml code compiled in - native code (and it is done in Coq (coqopt.out)). When compiling in - byte-code, the Coq system uses the -custom option in order to get an - autonomous executable (running independently of an ocaml implementation on - your computer). The way it works is that the .out file is composed of the - executable of the byte-code interpreter plus the byte-code for your own - program which is stored in the symbol table zone... stripping such an - executable, just remove your byte-code and consequentely cannot run - properly. - -Moreover the bytecode version is installed even on platforms having a -native version as the dynamic loading of tactics works only with the -bytecode version. +However, we recommend you to use the CoqIde GTK+ interface provided in coqide. diff --git a/debian/changelog b/debian/changelog index b51034f8..7c61421e 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.2.pl1+dfsg-3) UNRELEASED; urgency=low + + * Update README.Debian (Closes: #538398) + + -- Stephane Glondu <steph@glondu.net> Sat, 25 Jul 2009 16:31:48 +0200 + coq (8.2.pl1+dfsg-2) unstable; urgency=low * During validation of stdlib, call coqchk without -silent to avoid |