diff options
| author | herbelin | 2002-01-10 18:36:38 +0000 |
|---|---|---|
| committer | herbelin | 2002-01-10 18:36:38 +0000 |
| commit | e44d076a1aaaebe28cf9c1252db47fa7b7ca97ba (patch) | |
| tree | 2381fc5ca85af5ce44a2833652ad4ec4649efe03 | |
| parent | 8f3f0ddb911bd50522b6533b9f1ee03efad51a09 (diff) | |
Ajout flush
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2389 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/system.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/system.ml b/lib/system.ml index 37a102d40b..20f5f0ced2 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -56,6 +56,7 @@ let safe_getenv_def var def = Sys.getenv var with Not_found -> warning ("Environnement variable "^var^" not found: using '"^def^"' ."); + flush Pervasives.stdout; def let home = (safe_getenv_def "HOME" ".") |