summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--debian/README.Debian30
-rw-r--r--debian/changelog6
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