Merge branch 'dev'

Authored by cgilles on Jun 5 2020, 10:08 PM.