Merge branch 'master' into CB-12277 149/head
authorrussa <aaron.russ@dfki.de>
Tue, 22 May 2018 10:43:52 +0000 (12:43 +0200)
committerrussa <aaron.russ@dfki.de>
Tue, 22 May 2018 10:43:52 +0000 (12:43 +0200)
commitc95a26ab345606f83571795dd562c7a24074f469
tree13bb1302149236974402ea3b5e2e6463edbf4784
parentf9c88b8ab8280df920dc0de8e101a3abe599a353
parentd96c08e00badb5beca400abce4885bded56a03f7
Merge branch 'master' into CB-12277