diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2015-03-28 15:26:14 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2015-06-22 10:50:16 +0200 |
| commit | 333d41a9a28767ab146aab0527ff2b235bbd31a7 (patch) | |
| tree | e8ade79a927b0fb5546a179394629d0893fbc826 /toplevel/usage.ml | |
| parent | 851539eca5016da98253308749131abae3ec7b93 (diff) | |
All invocations to ocaml compilers go through ocamlfind
Nothing is done for camlp4
There is an issue with computing camlbindir
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 36ecc9fa5..c7d77de8c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -110,12 +110,7 @@ let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); - Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep; - Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc; - Printf.printf "OCAMLOPT=%s\n" Coq_config.ocamlopt; - Printf.printf "OCAMLDOC=%s\n" Coq_config.ocamldoc; - Printf.printf "CAMLBIN=%s/\n" (Envars.camlbin ()); - Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ()); + Printf.printf "OCAMLFIND=%s\n" (Envars.ocamlfind ()); Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; Printf.printf "CAMLP4O=%s\n" Coq_config.camlp4o; Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ()); |