Commit 7530368
committed
Properly flush -time-file at exit
Without this it's possible that some output will be omitted. For
instance ExtensionalFunctionRepresentative (1 command file in stdlib)
sometimes has no timing info.
We could try to explicitly call flushing after running coq eg in
ccompile, but getting all time-file users seems awkward and not worth
the bother.1 parent ebea542 commit 7530368
1 file changed
+9
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
40 | 40 | | |
41 | 41 | | |
42 | 42 | | |
43 | | - | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
44 | 52 | | |
45 | 53 | | |
46 | 54 | | |
| |||
0 commit comments