suggestion: timer format

[Markus Grassl <markus.grassl@ug.edu.pl>]

Hello,

I understand that the printing of timing information is hard-coded in 
the function 'convert_time' in the file 'gplib.c'.

In order to simplify the parsing of timing information, I suggest to 
make the format more flexible.
The user might want to switch the format using 'default'; e.g. printing 
in seconds only, or include zeros in the printing of minutes when the 
time exceeds one hour.



Best

Markus