"Time" output is lost when this is the last tactic before a "}"

[RalfJung]

I tried the following code:

Goal True ∧ True.
split. {
Time auto.

When I run this in coqtop, it prints something like

Finished transaction in 0. secs (0.u,0.s) (successful)
This subproof is complete, but there are some unfocused goals.
Try unfocusing with "}".

But when I do this in PG, it just shows

This subproof is complete, but there are some unfocused goals.
         Try unfocusing with "}".

It seems not possible to measure the time of the last tactic before a closing curly brace?

[Matafou]

Indeed the timing information is present in the coq buffer but it is not dispatched in response buffer. Probably because it is not enclosed inside a <infomsg> tag. I guess we should ask the coq team to categorize the message.