On Wed, Mar 13, 2019 at 1:26 PM Christoph Berg <myon(at)debian(dot)org> wrote:
> (This seems to be the only occurrence of this error, after about 2
> minutes of git-grep-ing.)
>
Thanks, pushed!
--
Magnus Hagander
Me: https://www.hagander.net/ <http://www.hagander.net/>
Work: https://www.redpill-linpro.com/ <http://www.redpill-linpro.com/>