diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 15:07:15 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 16:14:29 +0100 |
commit | 65d8cfc58068b95633106e6c2376f286fda88623 (patch) | |
tree | 6ad772c6e5032a40d6e6bca41bdacae687435a60 /clib/bigint.ml | |
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 'clib/bigint.ml')
0 files changed, 0 insertions, 0 deletions