aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-04 14:35:51 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:28 +0200
commitb2b4e85ec6607d7364a0da9c65ae9303b9f73c03 (patch)
tree5653b4d5438ddead97fd8c285c772c429a758511 /toplevel/usage.ml
parentda5ac9169d0c65ff389104dfd983311b85e059e2 (diff)
Usage.print_config moved to Envars
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml13
1 files changed, 0 insertions, 13 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e29048035..67701d73e 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -115,16 +115,3 @@ let print_usage_coqc () =
flush stderr ;
exit 1
-(* Print the configuration information *)
-
-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 "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 ());
- Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ());
- Printf.printf "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat;
- Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false")