Merge branch 'master' into terencehill/bot_ai
authorterencehill <piuntn@gmail.com>
Thu, 23 Jan 2020 10:18:55 +0000 (11:18 +0100)
committerterencehill <piuntn@gmail.com>
Thu, 23 Jan 2020 10:18:55 +0000 (11:18 +0100)

Trivial merge