aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index aa26075b7..eb58e67d0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -952,7 +952,7 @@ let print_summary () =
pr "\n";
pr " Architecture : %s\n" arch;
if operating_system <> "" then
- pr " Operating system : %s\n" operating_system;
+ pr " Operating system : %s\n" operating_system;
pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags);
pr " Other bytecode link flags : %s\n" custom_flag;
pr " OS dependent libraries : %s\n" osdeplibs;