aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-01-22 17:33:55 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-01-30 18:51:53 +0100
commitc734ccd8081e52ee5576d0efac9b065d4f37f7d5 (patch)
treef36a9b9d25627ecf323f782bc55edab6fa408754 /INSTALL
parent74bd95d10b9f4cccb4bd5b855786c444492b201b (diff)
Coqmktop without Sys.command, changes in ./configure -*byteflags options
NB: Please re-run ./configure after pulling this commit For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore, but rather CUnix.sys_command, which is based on Unix.create_process. This way, we do not need to bother with the underlying shell (/bin/sh or cmd.exe) and the way arguments are to be quoted :-). Btw, many cleanups of coqmktop. Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option" that collect as a string several sub-options to be given by coqmktop to ocamlc. For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to parse all these sub-options. To ease that, I've made the following changes to the ./configure options: * The -coqrunbyteflags and its blank-separated argument isn't accepted anymore, and is replaced by a new option -vmbyteflags which expects a comma-separated argument. For instance: ./configure -vmbyteflags "-dllib,-lcoqrun" Btw, on this example, the double-quotes aren't mandatory anymore :-) * The -coqtoolsbyteflags isn't accepted anymore. To the best of my knowledge, nobody ever used it directly (it was internally triggered as a byproduct of the -custom option). The only interest I can think of for this option was to cancel the default use of ocamlc custom-linking on Win32 and MacOS. For that, ./configure now provides a -no-custom option.
Diffstat (limited to 'INSTALL')
-rw-r--r--INSTALL2
1 files changed, 1 insertions, 1 deletions
diff --git a/INSTALL b/INSTALL
index a868f8fc8..ca8d705c5 100644
--- a/INSTALL
+++ b/INSTALL
@@ -315,7 +315,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
the directory of the standard library of OCaml;
- recompile your bytecode executables after reconfiguring the location of
of the shared library:
- ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ...
+ ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
where <path> is the directory where the dllcoqrun.so is installed;
- (not recommended) compile bytecode executables with a custom OCaml
runtime by using: