You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 

66 lines
2.0 KiB

  1. name: Deploy the documentation
  2. on:
  3. push:
  4. branches:
  5. # For bleeding-edge documentation
  6. - develop
  7. # For documentation specific to a release
  8. - 'release-v*'
  9. # stable docs
  10. - master
  11. workflow_dispatch:
  12. jobs:
  13. pages:
  14. name: GitHub Pages
  15. runs-on: ubuntu-latest
  16. steps:
  17. - uses: actions/checkout@v3
  18. - name: Setup mdbook
  19. uses: peaceiris/actions-mdbook@adeb05db28a0c0004681db83893d56c0388ea9ea # v1.2.0
  20. with:
  21. mdbook-version: '0.4.17'
  22. - name: Build the documentation
  23. # mdbook will only create an index.html if we're including docs/README.md in SUMMARY.md.
  24. # However, we're using docs/README.md for other purposes and need to pick a new page
  25. # as the default. Let's opt for the welcome page instead.
  26. run: |
  27. mdbook build
  28. cp book/welcome_and_overview.html book/index.html
  29. # Figure out the target directory.
  30. #
  31. # The target directory depends on the name of the branch
  32. #
  33. - name: Get the target directory name
  34. id: vars
  35. run: |
  36. # first strip the 'refs/heads/' prefix with some shell foo
  37. branch="${GITHUB_REF#refs/heads/}"
  38. case $branch in
  39. release-*)
  40. # strip 'release-' from the name for release branches.
  41. branch="${branch#release-}"
  42. ;;
  43. master)
  44. # deploy to "latest" for the master branch.
  45. branch="latest"
  46. ;;
  47. esac
  48. # finally, set the 'branch-version' var.
  49. echo "branch-version=$branch" >> "$GITHUB_OUTPUT"
  50. # Deploy to the target directory.
  51. - name: Deploy to gh pages
  52. uses: peaceiris/actions-gh-pages@bd8c6b06eba6b3d25d72b7a1767993c0aeee42e7 # v3.9.2
  53. with:
  54. github_token: ${{ secrets.GITHUB_TOKEN }}
  55. publish_dir: ./book
  56. destination_dir: ./${{ steps.vars.outputs.branch-version }}