diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-18 17:47:52 -0400 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-06 10:40:41 +0200 |
| commit | 32ed349b992710da136a443c8e0778a6346aa9a7 (patch) | |
| tree | 79ce1e49e6e5d90ed4a6f75c96804883d1c2a218 /configure.ml | |
| parent | 2df88d833767f6a43ac8f08627e1cb9cc0c8b30d (diff) | |
Fix indentation of configure printout
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 2 |
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; |