Performance optimisation - Use unordered_map in numbering instead of map - #5539
Merged
tautschnig merged 7 commits intoNov 10, 2020
Merged
unordered_map in numbering instead of map - #5539