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.2, 2023,
generated by texi2html.