Cherry-pick of "Merge branch 'DictDevel-master-20170428' into 'master'"

Dictionary Development, master branch (2017.04.28.)

See merge request !41 (merged)

This is to make the updated dictionary generation code in the 1.0 branch more CI friendly.