Commit a7201894 authored by François Bobot's avatar François Bobot

[Cpulimit] when stdout of why3-cpulimit is redirected to a file in some cases there is no flushing

parent 41ec8d66
......@@ -193,6 +193,7 @@ int main(int argc, char *argv[]) {
wall_time = (ull_stop.QuadPart - ull_start.QuadPart + 0.0) / 10000000.;
fprintf(stdout,
"why3cpulimit cpu time: %fs wall time: %fs\n", cpu_time, wall_time);
fflush(stdout);
}
CloseHandle(pi.hProcess);
CloseHandle(pi.hThread);
......
......@@ -56,6 +56,7 @@ int main(int argc, char *argv[]) {
time = (double)((tms.tms_cutime + tms.tms_cstime + 0.0)
/ sysconf(_SC_CLK_TCK));
fprintf(stdout, "why3cpulimit time : %f s\n", time);
fflush(stdout);
if (WIFEXITED(status)) return WEXITSTATUS(status);
kill(getpid(),SIGTERM);
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment