Remove unused parameter from cpp_destructor and fix types#2413
Merged
tautschnig merged 1 commit intodiffblue:developfrom Jun 25, 2018
Merged
Remove unused parameter from cpp_destructor and fix types#2413tautschnig merged 1 commit intodiffblue:developfrom
tautschnig merged 1 commit intodiffblue:developfrom