diff options
Diffstat (limited to 'debian/README.Debian')
| -rw-r--r-- | debian/README.Debian | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/README.Debian b/debian/README.Debian index 685f6047..d91bc559 100644 --- a/debian/README.Debian +++ b/debian/README.Debian @@ -28,7 +28,7 @@ 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 + 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 |