Merge branch 'develop' into releases/Release_2_11_Branch
authorJalview Development Admin <jalview-dev-owner@jalview.org>
Tue, 28 May 2019 12:43:21 +0000 (13:43 +0100)
committerJalview Development Admin <jalview-dev-owner@jalview.org>
Tue, 28 May 2019 12:43:21 +0000 (13:43 +0100)

Trivial merge