Remove unused and inconsistent pointer_object_has_type#2439
Merged
tautschnig merged 1 commit intodiffblue:developfrom Jul 7, 2018
Merged
Remove unused and inconsistent pointer_object_has_type#2439tautschnig merged 1 commit intodiffblue:developfrom
tautschnig merged 1 commit intodiffblue:developfrom