Merge branch 'trunk' into dev

Make sure all commits in trunk are also reflected in dev, so that
trunk does not have "extra" commits (granted, they are just merge
commits).