On Tuesday, 30 January 2024 at 04:35:45 pm GMT+3, Andrey M. Borodin <x4mmm@yandex-team.ru> wrote:
> On 30 Jan 2024, at 15:33, Junwang Zhao <zhjwpku@gmail.com> wrote: > > It's always good to add a newline at the end of a source file, though > this might be nitpicky.