From: Claudio Sacerdoti Coen Date: Mon, 27 Mar 2006 08:33:25 +0000 (+0000) Subject: Flush stdout added in proper position. X-Git-Tag: make_still_working~7460 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e8de117d3fe5e29364be56a9c084e954cb47869;p=helm.git Flush stdout added in proper position. --- diff --git a/helm/software/components/binaries/utilities/test_library.ml b/helm/software/components/binaries/utilities/test_library.ml index 8abf5e9be..f0e9510db 100644 --- a/helm/software/components/binaries/utilities/test_library.ml +++ b/helm/software/components/binaries/utilities/test_library.ml @@ -69,6 +69,7 @@ let _ = | _ -> assert false in Printf.printf "%s " uri; + flush stdout; let uri = UriManager.uri_of_string uri in let before = Unix.gettimeofday () in ignore (CicTypeChecker.typecheck uri);