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.3.1, 2022,
generated by texi2html.