Merge pull request #13299 from pgavlin/GH13161
authorPat Gavlin <pgavlin@gmail.com>
Thu, 10 Aug 2017 23:02:03 +0000 (16:02 -0700)
committerGitHub <noreply@github.com>
Thu, 10 Aug 2017 23:02:03 +0000 (16:02 -0700)
Fix issue #13161.


Trivial merge