Skip to content

Fix some rounding issues due to double promotion#1286

Merged
derselbst merged 1 commit intomasterfrom issue1284Dec 10, 2023