Re: [RFA 15/42] Remove merge_symbol_lists

Simon Marchi
2018-07-08T16:54:33Z

On 2018-05-23 12:58 AM, Tom Tromey wrote:
> I discovered that merge_symbol_lists is unused, so this removes it.

LGTM.