| Wed, 09 Jun 2021 10:52:37 +0200 | wenzelm | proper profiling within command execution: messages require PIDE id; | changeset | files |
| Wed, 09 Jun 2021 10:37:53 +0200 | wenzelm | more systematic treatment of profiling mode; | changeset | files |
| Tue, 08 Jun 2021 23:36:30 +0200 | wenzelm | tuned message; | changeset | files |