Tue, 13 Mar 2018 17:15:01 +0100 | wenzelm | more flexible preferences: avoid hardwired file; | changeset | files |
Tue, 13 Mar 2018 17:13:20 +0100 | wenzelm | tuned; | changeset | files |
Tue, 13 Mar 2018 16:08:13 +0100 | wenzelm | more operations for typed JSON values; | changeset | files |