aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-03-29 18:02:46 +0200
committerPierre-Marie Pédrot2020-04-26 14:24:48 +0200
commit75e394770b534994830f6d80e649734275de5006 (patch)
tree375b3fd6e78384d13ad7027876ace4bb6af04015 /configure.ml
parent6c15158c5ab1693868356e4b2433c7eb7b8ec3f2 (diff)
Implement a name-based representation for vo files.
See CEP#44 for futher details.
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 282b40db27..0eff70999d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1059,6 +1059,7 @@ 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_i32 = pr "let %s = %dl\n" in
let pr_p s o = pr "let %s = %S\n" s
(match o with Relative s -> s | Absolute s -> s) in
let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in
@@ -1086,7 +1087,7 @@ let write_configml f =
pr_s "exec_extension" exe;
pr "let gtk_platform = `%s\n" !idearchdef;
pr_b "has_natdynlink" hasnatdynlink;
- pr_i "vo_magic_number" vo_magic;
+ pr_i32 "vo_version" vo_magic;
pr_i "state_magic_number" state_magic;
pr_s "browser" browser;
pr_s "wwwcoq" !prefs.coqwebsite;