diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-11 13:55:25 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-13 12:45:31 +0100 |
| commit | 815bdef747f7d69f25121f42ec72d109ec92edfe (patch) | |
| tree | 4db845dff85346033fee6746b7087acd4d6a033d /configure.ml | |
| parent | 8cb2b6a00d71572d60d4dcc4e7ec697fd3933389 (diff) | |
[Sphinx] Read version number from configure
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/configure.ml b/configure.ml index 4726831e4..6c052b63b 100644 --- a/configure.ml +++ b/configure.ml @@ -1371,3 +1371,13 @@ let write_macos_metadata exec = let () = if arch = "Darwin" then List.iter write_macos_metadata distributed_exec + +let write_configpy f = + safe_remove f; + let o = open_out f in + let pr s = fprintf o s in + let pr_s = pr "%s = '%s'\n" in + pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure\n"; + pr_s "version" coq_version + +let _ = write_configpy "config/coq_config.py" |