Getting devel and master in sync

The last couple of pull requests have gone straight to `master` instead of `devel`. I did not catch these and as such, `master` is ahead of `devel`. Since we're using the gitflow workflow, our main working branch should always be `devel`. Since these are pretty straightforward changes, this PR is just to get them in sync.