| Fri, 15 Nov 2024 13:31:36 +0100 | wenzelm | more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling); | changeset | files |
| Fri, 15 Nov 2024 13:08:48 +0100 | wenzelm | less ambitious selection; | changeset | files |
| Fri, 15 Nov 2024 21:37:26 +0100 | nipkow | mv Discrete to Discrete_Cpo to avoid theory name clashes | changeset | files |
| Thu, 14 Nov 2024 11:33:51 +0100 | wenzelm | disable 2d9b6e32632d for now: unknown problems on macOS; | changeset | files |