gitignore the Jekyll output directory even if you run Jekyll from the repo root.
gitignore the WASM file since it's a build output.
Delete tools/scripts/serve_docs.sh - it's no longer needed since Jekyll 4.3.0 which fixed the Content-Type for WASM files (https://github.com/jekyll/jekyll/pull/8965) 4.3.0 was released October 2020.
In push_docs, when checking out the repo to the working directory, directly check out the gh-pages branch instead of checking out HEAD and then switching branch.
Various minor changes:
tools/scripts/serve_docs.sh- it's no longer needed since Jekyll 4.3.0 which fixed the Content-Type for WASM files (https://github.com/jekyll/jekyll/pull/8965) 4.3.0 was released October 2020.