Merge remote-tracking branch 'upstream/dev' into dev
authorVincent Torri <vincent.torri@gmail.com>
Sun, 2 Dec 2018 18:42:38 +0000 (19:42 +0100)
committerVincent Torri <vincent.torri@gmail.com>
Sun, 2 Dec 2018 18:42:38 +0000 (19:42 +0100)

Trivial merge