diff options
| author | Maxime Dénès | 2018-03-06 15:07:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-06 16:14:29 +0100 |
| commit | 65d8cfc58068b95633106e6c2376f286fda88623 (patch) | |
| tree | 6ad772c6e5032a40d6e6bca41bdacae687435a60 /dev | |
| parent | 67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff) | |
Add some missing flushes in configure.
Some messages were sometimes not printed because of the missing flushes.
We use a generic combinator suggested by Emilio.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions