diff options
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" |