Fri, 23 Aug 2024 14:41:45 +0200 | wenzelm | tuned signature: separate markup vs. extern; | changeset | files |
Fri, 23 Aug 2024 13:28:01 +0200 | wenzelm | clarified signature; | changeset | files |
Thu, 22 Aug 2024 17:12:32 +0200 | wenzelm | tuned: prefer configuration options via context; | changeset | files |
Thu, 22 Aug 2024 16:04:06 +0200 | wenzelm | tuned; | changeset | files |
Thu, 22 Aug 2024 15:57:30 +0200 | wenzelm | tuned signature: more operations; | changeset | files |
Fri, 23 Aug 2024 18:40:12 +0200 | nipkow | tuned comments | changeset | files |