Commit 3e6a9045213268089b567d7a6f7ccf30374b32b7

Patrick Steinhardt 2019-12-13T08:53:51

Merge pull request #5320 from josharian/minor-docs Minor doc improvements