{"push_id":1257135034,"size":1,"distinct_size":1,"ref":"refs/heads/time_print_fix","head":"adfdd36a15052175fc1217f6a6ded37a0d6d4e00","before":"77f2ba86fcca499160953a0f5a9f50a63580c29b","commits":[{"sha":"adfdd36a15052175fc1217f6a6ded37a0d6d4e00","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[pp] Fix bug 4842 (Time prints in multiple lines)\n\nThis commit proposes a fix for\nhttps://coq.inria.fr/bugs/show_bug.cgi?id=4842\n\nThe previous feature is a bit complicated to do correctly due to the\nseparation over who has control of the console.\n\nIndeed, `-timed` is a command line option of the batch compiler, so we\nresort to a hack and assume control over the console. I am not very\nhappy with this solution but should do the job.\n\nNote that the timing event is still being sent by the standard msg\nmechanism. A particular point of interest is the duplication of paths\nbetween the stm and vernac.","distinct":true,"url":"https://api.github.com/repos/ejgallego/coq/commits/adfdd36a15052175fc1217f6a6ded37a0d6d4e00"}]}
{"actor":{"display_login":"ejgallego"}}