diff options
| author | Pierre-Marie Pédrot | 2014-01-24 23:40:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-24 23:40:57 +0100 |
| commit | 30986b6e7616e9c170b012bb00dff80603d84c76 (patch) | |
| tree | b52fd192e834b1a7cd3117025f66fedd503efd29 | |
| parent | c6794b4f09a371a513ddd27818d4392b8340f250 (diff) | |
The configure script now outputs the parameters it was fed with in
config/coq_config.ml
| -rw-r--r-- | configure.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 50ad264993..d18c0663c6 100644 --- a/configure.ml +++ b/configure.ml @@ -949,7 +949,9 @@ let write_configml f = let pr_o s o = pr "let %s = %s\n" s (match o with None -> "None" | Some d -> sprintf "Some %S" d) in - pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n\n"; + pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; + pr "(* Exact command that generated this file: *)\n"; + pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); pr_b "local" !Prefs.local; pr_s "coqrunbyteflags" coqrunbyteflags; pr_o "coqlib" (if !Prefs.local then None else Some libdir); |