Disable search index to unblock docs pipeline (#170)

Author: rcoh

.github/workflows/docs.yaml

@@ -28,6 +28,8 @@ jobs:
           ls
           rm -rf docs
           mv docs-new/doc docs
+          # temporary hack since this file is too large for GitHub pages
+          rm docs/search-index.js
           git config --local user.email "[email protected]"
           git config --local user.name "GitHub Action (docs)"
           git add docs