[pp] Fix bug 4842 (Time prints in multiple lines)

This commit proposes a fix for
https://coq.inria.fr/bugs/show_bug.cgi?id=4842

The previous feature is a bit complicated to do correctly due to the
separation over who has control of the console.

Indeed, `-timed` is a command line option of the batch compiler, so we
resort to a hack and assume control over the console. I am not very
happy with this solution but should do the job.

Note that the timing event is still being sent by the standard msg
mechanism. A particular point of interest is the duplication of paths
between the stm and vernac.

0 files changed, 0 insertions, 0 deletions