deal with unwanted side-effects of #3006#5336

Merged

fingolfin merged 1 commit intogap-system:masterfrom ThomasBreuer:TB_nice_basis_filter

Jan 19, 2023

+9-5

Commits on Jan 19, 2023

deal with unwanted side-effects of gap-system#3006
ThomasBreuer
committed