morris 98e19b3355 Merge branch 'contrib/github_pr_8496' into 'master' 3 lat temu
..
hal 98e19b3355 Merge branch 'contrib/github_pr_8496' into 'master' 3 lat temu