GNU bug report logs - #76601
[PATCH 0/1] dir-locals: Add copyrights.

Previous Next

Full log

Message #32 received at 76601 <at> debbugs.gnu.org (full text, mbox):

From: Tomas Volf <~@wolfsden.cz>
To: Denis 'GNUtoo' Carikli <GNUtoo <at> cyberdimension.org>
Cc: 76601 <at> debbugs.gnu.org
Subject: Re: [bug#76601] [PATCH v2] dir-locals: Add copyrights.
Date: Wed, 19 Mar 2025 17:46:57 +0100

Denis 'GNUtoo' Carikli <GNUtoo <at> cyberdimension.org> writes:

> We also have merge commits:
>> $ git log --pretty='format:%h %ad %an <%ae>' origin/master \
>> --date="format:%Y" --merges -- .dir-locals.el 
>> c4133c43c7 2021 Marius Bakke <marius <at> gnu.org> 
>> 0e47fcced4 2021 Ludovic Courtès <ludo <at> gnu.org>
>> 129b9b16d9 2020 Maxim Cournoyer <maxim.cournoyer <at> gmail.com>
>
> But didn't see anything touching .dir-locals.el with 'git show
> c4133c43c7', so I didn't include Marius Bakke, so it would be good if
> you can verify if my theory is right.

Yes, I have encountered the commit as well during the verification and
arrived to the same conclusion (== he modified nothing).  I do not
understand why the commit is listed.

I think it looks good now, I have added my reviewed-by reply to the bug
and applied the appropriate user tag, so hopefully some committer will
pick it up.  ^_^

Have a nice day,
Tomas

-- 
There are only two hard things in Computer Science:
cache invalidation, naming things and off-by-one errors.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.