Thanks very much -- I ended up making these changes in another branch so I could merge them against develop instead of master. That nudged me to change the default branch in Github to develop, so your PR was useful in that way, too. I'll credit you in the release notes for the next version.
Thanks very much -- I ended up making these changes in another branch so I could merge them against
developinstead ofmaster. That nudged me to change the default branch in Github todevelop, so your PR was useful in that way, too. I'll credit you in the release notes for the next version.