Re: Remove duplicate history entries in command buffer

[Pavel Sanda]

On Mon, Jul 11, 2022 at 10:53:23AM +0200, Kornel Benko wrote:
> So the outcome may be a new preference?

Please no.

Pavel
-- 
lyx-devel mailing list
lyx-devel@lists.lyx.org
http://lists.lyx.org/mailman/listinfo/lyx-devel