Use std::set instead of map as value is never used#2408

Merged

tautschnig merged 1 commit intodiffblue:developfrom

tautschnig:vs-set-map

Jun 25, 2018

Commits on Jun 23, 2018

Use std::set instead of map as value is never used
tautschnig
committed