diff options
| author | Gaëtan Gilbert | 2018-06-03 15:29:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-06-03 15:29:24 +0200 |
| commit | 8c99ee9b5b1212bf52fdf580525489eb8f89a682 (patch) | |
| tree | 333e46afd80ddd9ab51c452fb611d58d9a170e31 | |
| parent | 582c1d2d152b696d0b7ec1ec8240436ae66ff326 (diff) | |
configure: fix warning printing
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 45c3bb67a4..933143e682 100644 --- a/configure.ml +++ b/configure.ml @@ -33,7 +33,7 @@ let cprintf s = cfprintf stdout s let ceprintf s = cfprintf stderr s let die msg = ceprintf "%s%s%s\nConfiguration script failed!" red msg reset; exit 1 -let warn s = cprintf ("%sWarning: " ^^ s ^^ "%s") yellow reset +let warn s = kfprintf (fun oc -> cfprintf oc "%s" reset) stdout ("%sWarning: " ^^ s) yellow let s2i = int_of_string let i2s = string_of_int |