On Fri, Nov 02, 2018 at 10:49:23AM +0100, Branko Čibej wrote: > On 02.11.2018 10:44, Stefan Sperling wrote: > > I confirm that your patch is correct. I mis-indented these blocks. > > Time to start using a real editor, I guess? :)
The further I progress into adulthood, the more our tiny indentation by two spaces seems to be causing me trouble... Maybe(we) could have another (historical) vote, on tabs vs spaces this time? Disclaimer: I'd vote for tabs :)
