| Wed, 01 Feb 2023 15:39:48 +0100 | wenzelm | clarified GUI; | changeset | files |
| Wed, 01 Feb 2023 13:50:53 +0100 | wenzelm | clarified GUI: omit pointless search buttons, as real output is shown as markup; | changeset | files |
| Wed, 01 Feb 2023 10:54:29 +0100 | wenzelm | more uniform use of Symbol.output, even in situations where its Symbol.encode is usually redundant; | changeset | files |