From 816ae8c64624eee082a54c04b1f4e72e3426d265 Mon Sep 17 00:00:00 2001
From: courant
Date: Tue, 24 Apr 2001 15:07:41 +0000
Subject: ajout necessaire pour paquet debian

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1688 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 distrib/debian/README.Debian | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 distrib/debian/README.Debian

(limited to 'distrib/debian/README.Debian')

diff --git a/distrib/debian/README.Debian b/distrib/debian/README.Debian
new file mode 100644
index 0000000000..7dc4ee03d5
--- /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.
-- 
cgit v1.2.3