aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross2016-06-18 17:47:52 -0400
committerMaxime Dénès2016-07-06 10:40:41 +0200
commit32ed349b992710da136a443c8e0778a6346aa9a7 (patch)
tree79ce1e49e6e5d90ed4a6f75c96804883d1c2a218
parent2df88d833767f6a43ac8f08627e1cb9cc0c8b30d (diff)
Fix indentation of configure printout
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index aa26075b74..eb58e67d09 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;