Hi @boudreau, is there any reason to keep this MR unmerged? Shall we just go ahead and merge it? Thanks.
mentioned in commit d3d7949c
merged
