23 Apr
2019
23 Apr
'19
11:23 a.m.
Oops, a mistake in the previous post. Should be… Maybe a new statistics option is desirable; statistics <surface-length on/off>, with the default [off] matching the current behaviour