a git diff is used to show the differences between the rendered docs in the target vs the PR, and hidden behind an expandable box (tested via #136)
A PR that has docs changes and then doesn't have any more will not correctly unpublish the site and remove the PR comment (tested via #137)
^ this can happen if a PR was not rebased against a newer version of main that has docs changes, or can happen when changes to docs (intentional or accidental) in a PR are removed in a later commit, so that there is no longer any doc change.
SUMMARY
Changes to docs build:
git diffis used to show the differences between the rendered docs in the target vs the PR, and hidden behind an expandable box (tested via #136)mainthat has docs changes, or can happen when changes to docs (intentional or accidental) in a PR are removed in a later commit, so that there is no longer any doc change.ISSUE TYPE
COMPONENT NAME
ADDITIONAL INFORMATION