On Tue, Jan 16, 2018 at 14:42:32 +0100, Cristian Adam wrote: > I don't know why it wasn't a pull request on gitlab though. > Thu, 30 Jun 2016 12:24:02 -0700 This predates Gitlab usage for patch submission (which started around July 2016). --Ben