Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Add opts in doc 2 #1763
Having skimmed the diff, all the changes look correct to me. As the tests are green, I think it is better to merge sooner than later. I'm sure there will be other places that
@jordansamuels Thanks again for this PR! Merging.