diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-24 23:06:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-24 23:06:42 +0000 |
| commit | 9007bc92139cb80139337ea5d11322c1c1f12c19 (patch) | |
| tree | b5a8d6e11caba332336741438ed0891555b730d7 | |
| parent | 717d24bdb9beeeceb5f39954fb5d81d4a7d81a67 (diff) | |
Ajout flush, divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1276 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | lib/system.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/system.ml b/lib/system.ml index b743df478..ae7784bf5 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -36,8 +36,8 @@ let all_subdirs root alias = traverse file newrel end with Unix_error (e,s1,s2) -> - Printf.printf "Error while scanning load path:\n %s: %s\n" - s2 (error_message e) + (Printf.printf "Warning while scanning load path:\n%s: %s\n" + s2 (error_message e); flush Pervasives.stdout) done with End_of_file -> closedir dirh |