Skip to content

Better decimal rounding in the NumberInput widget#457

Merged
mfish33 merged 8 commits intomasterfrom
rounded-zoom-numbering
Jan 7, 2022
Merged

Better decimal rounding in the NumberInput widget#457
mfish33 merged 8 commits intomasterfrom
rounded-zoom-numbering

Commits

Commits on Dec 30, 2021

Commits on Jan 3, 2022

Commits on Jan 7, 2022