export-file-local_symbols:: update base name and pretty name#6337

Merged

tautschnig merged 1 commit intodiffblue:developfrom

tautschnig:fix-6330

Oct 24, 2022

Commits on Oct 24, 2022

export-file-local_symbols:: update base name and pretty name
tautschnig
committed