Wed, 04 Sep 2024 12:50:52 +0200 | wenzelm | more accurate Default_Metric; | changeset | files |
Mon, 02 Sep 2024 22:41:23 +0200 | wenzelm | tuned signature; | changeset | files |
Mon, 02 Sep 2024 22:00:53 +0200 | wenzelm | clarified output_spaces, based on Output.output_width; | changeset | files |