Fix variants with <digit>.</digit> are extracted correctly#17153
Merged
RobinMalfait merged 5 commits intomainfrom Mar 12, 2025
Merged
Fix variants with `<digit>.</digit>` are extracted correctly#17153RobinMalfait merged 5 commits intomainfrom
RobinMalfait merged 5 commits intomainfrom
Commits
Commits on Mar 12, 2025
- committed
- committed
- committed
- committed
- committed
