ajout necessaire pour paquet debian

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1688 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 0 deletions

diff --git a/distrib/debian/README.Debian b/distrib/debian/README.Debian
new file mode 100644
index 000000000..7dc4ee03d
--- /dev/null
+++ b/distrib/debian/README.Debian
@@ -0,0 +1,16 @@
+Coq package for Debian
+----------------------
+
+As an unusual thing, some files (*.out) in this package need to be left
+'unstripped' after compiling. The reason, as explained by the authors, 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.