diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-12 03:08:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 12:12:56 +0200 |
| commit | d53ba17d1761261593c598b6a88cfd6ce0eb3514 (patch) | |
| tree | df442236534c337d8eaba771ff15bebf4e806240 /configure.ml | |
| parent | 34a2f9eb315da8b794f2573bdfc8ff941d81bdbe (diff) | |
Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.
This goes towards an approach where a local layout can be seen as an
installed layout.
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/configure.ml b/configure.ml index 1d2003501..1a851ef45 100644 --- a/configure.ml +++ b/configure.ml @@ -1022,15 +1022,12 @@ let write_configml f = let pr_s = pr "let %s = %S\n" in let pr_b = pr "let %s = %B\n" in let pr_i = pr "let %s = %d\n" in - 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"; 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 "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n"; - pr_o "coqlib" (if !Prefs.local then None else Some coqlib); + pr_s "coqlib" coqlib; pr_s "configdir" configdir; pr_s "datadir" datadir; pr_s "docdir" docdir; |