identical to timer (see timer), except that real times (i.e.,
wall-clock) times are reported, instead of CPU times. This can be
trusted on all operating systems (including Windows95/98).
User manual for Singular version 4-0-3, 2016,
generated by texi2html.