Clear our destination directories before copying files to GitHub pages. (#10869)

This should fix stale deleted files being still accessible.
3 years ago · ebd8baf61f
parent ba7a91aea5
commit ebd8baf61f
2 changed files with 1 additions and 1 deletions
--- a/.github/workflows/docs.yaml
+++ b/.github/workflows/docs.yaml
@ -61,6 +61,5 @@ jobs:
        uses: peaceiris/actions-gh-pages@068dc23d9710f1ba62e86896f84735d869951305 # v3.8.0
        with:
          github_token: ${{ secrets.GITHUB_TOKEN }}
-          keep_files: true
          publish_dir: ./book
          destination_dir: ./${{ steps.vars.outputs.branch-version }}
--- a/changelog.d/10869.doc
+++ b/changelog.d/10869.doc
@ -0,0 +1 @@
+Properly remove deleted files from GitHub pages when generating the documentation.
				`@ -0,0 +1 @@`
				`Properly remove deleted files from GitHub pages when generating the documentation.`