diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-13 17:12:27 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-11-13 17:12:27 +0000 |
| commit | 8d41b4a80e6b1a944772a435e2a8eb54adc3048c (patch) | |
| tree | f9d8c36707503fc7bdd009f6f9f49bb81dd7eeb9 /toplevel | |
| parent | 6c79471f2d1f358b51ba367b094d4b01486a490c (diff) | |
Tentative d'amélioration de la robustesse des Makefile générés par
coq_makefile en présence de fichiers .ml :
- ajout d'une option -config à coqtop qui affiche les informations
de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN,
LOCAL)
- coq_makefile inclut un fichier Makefile.config qui contient les
valeurs des variables sus-mentionnées
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 15 | ||||
| -rw-r--r-- | toplevel/usage.mli | 3 |
3 files changed, 20 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 277bc8d09..2ad5117b9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -276,6 +276,8 @@ let parse_args is_ide = | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 + | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0 + | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 417a496f8..02fa69142 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -49,6 +49,7 @@ let print_usage_channel co command = -byte run the bytecode version of Coq -where print Coq's standard library location and exit + -config print Coq's configuration information and exit -v print Coq version and exit -q skip loading of rcfile @@ -84,3 +85,17 @@ options are: -bindir override the default directory where coqc looks for coqtop -image f specify an alternative executable for Coq -t keep temporary files\n\n" + +(* 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 "COQBIN=%s/\n" Coq_config.bindir; + Printf.printf "COQLIB=%s/\n" Coq_config.coqlib; + Printf.printf "COQTOP=%s/\n" Coq_config.coqtop; + Printf.printf "CAMLBIN=%s/\n" Coq_config.camldir; + Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; + Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib + + + diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 6c9ed474c..fb973e3ba 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -18,3 +18,6 @@ val print_usage : string -> unit (*s Prints the usage on the error output. *) val print_usage_coqtop : unit -> unit val print_usage_coqc : unit -> unit + +(*s Prints the configuration information *) +val print_config : unit -> unit |