closes #1893#1900

Merged

GillesDuvert merged 1 commit intognudatalanguage:masterfrom

GillesDuvert:revert_mostly_1891_and_patch_1893

Nov 2, 2024

Commits on Nov 1, 2024

reverting #1891 except for the sole location it is important (line 1580)
GillesDuvert
committed