aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-01-24 14:25:09 +0100
committerEmilio Jesus Gallego Arias2019-01-24 14:25:09 +0100
commitea6c157e7a47039d2c1505e896dbdd099a0da450 (patch)
tree6bf2035eee82d12be341602edb3653991399cb07 /configure.ml
parentf5241b99bb15f019eb629a7f24f2993f011e7e06 (diff)
parentaa4f1346e7cf2f8424259143d7aca6a883d3f9d2 (diff)
Merge PR #9372: [thread] protect threads against sigalrm
Reviewed-by: ejgallego
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/configure.ml b/configure.ml
index 33f76078cf..6f5ade3b9a 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1001,6 +1001,7 @@ let print_summary () =
pr " Architecture : %s\n" arch;
if operating_system <> "" then
pr " Operating system : %s\n" operating_system;
+ pr " Sys.os_type : %s\n" Sys.os_type;
pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags);
pr " Other bytecode link flags : %s\n" custom_flag;
pr " OCaml version : %s\n" caml_version;