Thu, 07 Nov 2024 15:42:35 +0100 | wenzelm | tuned: fewer warnings in IntelliJ IDEA; | changeset | files |
Thu, 07 Nov 2024 13:30:40 +0100 | wenzelm | clarified signature: more accurate types; | changeset | files |
Thu, 07 Nov 2024 13:26:31 +0100 | wenzelm | tuned signature: more standard names; | changeset | files |
Thu, 07 Nov 2024 13:22:59 +0100 | wenzelm | more uniform pretty_text_area.zoom via its zoom_component; | changeset | files |
Thu, 07 Nov 2024 12:35:55 +0100 | wenzelm | tuned signature; | changeset | files |
Thu, 07 Nov 2024 12:32:44 +0100 | wenzelm | tuned signature: more standard names; | changeset | files |