[Pkg-ocaml-maint-commits] [SCM] coq packaging branch, master, updated. debian/8.2.pl1+dfsg-2-1-gee2bd35

[Stephane Glondu]

The following commit has been merged in the master branch:
commit ee2bd359557ca6d68a5ca4aced4014f9e3581cbb
Author: Stephane Glondu <steph at glondu.net>
Date:   Sat Jul 25 16:33:09 2009 +0200

    Update README.Debian (Closes: #538398)

diff --git a/debian/README.Debian b/debian/README.Debian
index d91bc55..7da3eb6 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 b51034f..7c61421 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 at 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

-- 
coq packaging