fix typo in docs

[bakkot]

I think the HTML probably needs to be rebuilt too, but I couldn't figure out how to do it. There's no script in package.json which is suggestive of "this will rebuild the docs". I looked in "gulpfile.js", which seems to be used to handle various build tasks, but the only obvious task there is "docs", and attempting to run that fails with

[17:04:47] Starting 'docfx'...
/bin/sh: docfx: command not found
[17:04:47] 'docfx' errored after 6.18 ms

at which point I gave up.

[rbuckton]

docfx is an external documentation tool that's not available on NPM: https://dotnet.github.io/docfx/