diff options
| author | Pierre Boutillier | 2015-03-28 15:26:14 +0100 |
|---|---|---|
| committer | Pierre Boutillier | 2015-06-22 10:50:16 +0200 |
| commit | 333d41a9a28767ab146aab0527ff2b235bbd31a7 (patch) | |
| tree | e8ade79a927b0fb5546a179394629d0893fbc826 /lib/flags.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 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 009caa9dee..fe580b7fff 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -193,9 +193,9 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing camlbin (used by coqmktop) *) -let camlbin_spec = ref false -let camlbin = ref Coq_config.camlbin +(* Options for changing ocamlfind (used by coqmktop) *) +let ocamlfind_spec = ref false +let ocamlfind = ref Coq_config.camlbin (* Options for changing camlp4bin (used by coqmktop) *) let camlp4bin_spec = ref false |