From 6e8de117d3fe5e29364be56a9c084e954cb47869 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Mar 2006 08:33:25 +0000 Subject: [PATCH] Flush stdout added in proper position. --- helm/software/components/binaries/utilities/test_library.ml | 1 + 1 file changed, 1 insertion(+) 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); -- 2.39.5