A recent PR was merged to main causing the Documentation github action to fail. This would have been avoided had we run the documentation github action on all PRs (although without actually publishing the docs from the branch). This PR aims to fix this.
A recent PR was merged to main causing the Documentation github action to fail. This would have been avoided had we run the documentation github action on all PRs (although without actually publishing the docs from the branch). This PR aims to fix this.