>> I had another look and was about to merge.
>> But then I saw that your commits were attributed to Vigdis.
>
>> Maybe that was not on purpose since we usually use a common identity for
>> that. See https://tails.boum.org/contribute/git/#index3h2.
>
>> I don't mind either option but I wanted an acknowledgment from your side
>> first.
I didn't got an answer from Vigdis regarding the correct name to use in
the commit message, and anonym didn't finish his branch on time to be in
Tails 0.20.1, so I finished the branch, attributed the commits to "Tails
developers" and pushed all that into master.
I think that was not tracked in Redmine.
Thanks, for getting this moved forward Vigdis!