Increased admontion borders #647
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Deploy to GitHub Pages | |
| on: | |
| push: #Action fires anytime there is a push to the following branches | |
| branches: | |
| - main | |
| - development | |
| pull_request: #Action also fires anytime a PR is (re)opened, closed or synchronized | |
| types: | |
| - opened | |
| - reopened | |
| - synchronize | |
| - closed | |
| workflow_dispatch: #Action can also be triggered manually | |
| env: | |
| TZ: Australia/Canberra | |
| permissions: | |
| pull-requests: write # to comment on PRs | |
| pages: write # to deploy to Pages | |
| id-token: write # to verify the deployment originates from an appropriate source | |
| jobs: | |
| preview-setup: | |
| # If the action is fired because of a PR, run this job | |
| if: ${{ github.event_name == 'pull_request' }} | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Set up PR preview title | |
| # Set up infos for PR (new, updated or reopened branch not having a head as 'development' or 'main' branch) | |
| if: ${{ github.event.pull_request.head.ref != 'development' && github.event.pull_request.head.ref != 'main' }} | |
| run: | | |
| echo 'TITLE=PR preview' >> $GITHUB_ENV | |
| - name: Set up development preview title | |
| # Set up infos for PR (new, updated or reopened branch not having a head as 'development' or 'main' branch) | |
| if: ${{ github.event.pull_request.head.ref == 'development' }} | |
| run: | | |
| echo 'TITLE=Development website preview' >> $GITHUB_ENV | |
| - name: Get date | |
| run: echo "DATE=$(date '+%Y-%m-%d %H:%M %Z')" >> $GITHUB_ENV | |
| - name: Set up open PR message | |
| if: ${{ github.event.action != 'closed' }} | |
| run: | | |
| MULTI_LINES_TEXT="${{ env.TITLE }}\n | |
| :---:\n | |
| 🛫 Deployment still ongoing.<br> | |
| Preview URL will be available at the end of the deployment.\n | |
| For more information, please check the [Actions](https://github.com/${{ github.repository }}/actions) tab.\n | |
| ${{ env.DATE }}" | |
| echo "MSG<<EOF" >> $GITHUB_ENV | |
| echo -e $MULTI_LINES_TEXT >> $GITHUB_ENV | |
| echo "EOF" >> $GITHUB_ENV | |
| - name: Set up closed PR message | |
| if: ${{ github.event.action == 'closed' }} | |
| run: | | |
| MULTI_LINES_TEXT="${{ env.TITLE }}\n | |
| :---:\n | |
| 🛬 Preview link removed because the pull request was closed." | |
| echo "MSG<<EOF" >> $GITHUB_ENV | |
| echo -e $MULTI_LINES_TEXT >> $GITHUB_ENV | |
| echo "EOF" >> $GITHUB_ENV | |
| - name: Set preview | |
| uses: thollander/[email protected] | |
| with: | |
| comment_tag: pr-preview | |
| pr_number: ${{ github.event.number }} | |
| message: ${{ env.MSG }} | |
| build: | |
| # Cancel any previous build/deploy jobs that are still running (no need to build/deploy multiple times) | |
| concurrency: | |
| group: build-deploy | |
| cancel-in-progress: true | |
| runs-on: ubuntu-latest | |
| outputs: | |
| pr_nums: ${{ steps.build.outputs.pr_nums }} | |
| url: ${{ steps.url.outputs.url }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@master | |
| with: | |
| ref: main | |
| - name: Get URL | |
| id: url | |
| run: echo "url=$(ruby -r yaml -e 'puts YAML.load_file(ARGV[0])["site_url"]' mkdocs.yml)" >> "$GITHUB_OUTPUT" | |
| - name: Python setup | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: 3.9.x | |
| - name: Install dependencies | |
| run: pip install -r requirements.txt | |
| # Build full website using main, development and open PRs head branches | |
| # (excluding `development` and `main` as PR head branches) | |
| - name: Build full website | |
| env: | |
| GH_TOKEN: ${{ github.token }} # Required for gh usage | |
| id: build | |
| shell: bash | |
| run: | | |
| git fetch --all -Pp | |
| echo "Build main website" | |
| git checkout main | |
| mkdocs build -f mkdocs.yml -d ../website | |
| echo "Build development website" | |
| git checkout development | |
| mkdocs build -f mkdocs.yml -d ../website/development-website | |
| echo "Build PR websites" | |
| open_pr_info=$(gh pr list --json headRefOid,number,headRefName --jq '.[] | select(.headRefName!="development" and .headRefName!="main")') | |
| pr_nums=($(jq '.number' <<< "$open_pr_info")) | |
| pr_sha=($(jq -r '.headRefOid' <<< "$open_pr_info")) | |
| if [[ -n $pr_nums ]]; then | |
| echo "Found PR numbers: $(perl -pe 's/\s(?!$)/, /g' <<< ${pr_nums[@]})." | |
| echo "pr_nums=[$(perl -pe 's/\s(?!$)/,/g' <<< ${pr_nums[@]})]" >> "$GITHUB_OUTPUT" | |
| for i in ${!pr_nums[@]}; do | |
| git checkout ${pr_sha[i]} | |
| mkdocs build -f mkdocs.yml -d ../website/pr-preview/pr-${pr_nums[i]} | |
| done | |
| else | |
| echo "No open PR found." | |
| fi | |
| chmod -c -R +rX ../website | |
| - name: Create artifact for deployment to GitHub Pages | |
| uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa #v3.0.1 | |
| with: | |
| path: ../website | |
| deploy: | |
| needs: build | |
| runs-on: ubuntu-latest | |
| # Cancel any previous build/deploy jobs that are still running (no need to build/deploy multiple times) | |
| concurrency: | |
| group: build-deploy | |
| cancel-in-progress: true | |
| outputs: | |
| success: ${{ steps.success.outputs.success }} | |
| steps: | |
| - name: Deploy to GitHub Pages | |
| uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e #v4.0.5 | |
| - name: Output success status | |
| id: success | |
| run: | | |
| echo "success=1" >> "$GITHUB_OUTPUT" | |
| # Set pr-preview URL | |
| pr-preview: | |
| needs: [build, deploy] | |
| # If there are open PRs (whose head branch is neither `development` nor `main`), run this job | |
| if: ${{ needs.build.outputs.pr_nums }} | |
| runs-on: ubuntu-latest | |
| # Run the same job for each of the open PRs found | |
| strategy: | |
| matrix: | |
| pr_nums: ${{fromJson(needs.build.outputs.pr_nums)}} | |
| steps: | |
| - name: Get date | |
| run: echo "DATE=$(date '+%Y-%m-%d %H:%M %Z')" >> $GITHUB_ENV | |
| - name: Set pr-preview URL | |
| if: ${{github.event.action != 'closed'}} | |
| uses: thollander/[email protected] | |
| with: | |
| comment_tag: pr-preview | |
| pr_number: ${{ matrix.pr_nums }} | |
| message: "\ | |
| PR Preview | |
| :---: | |
| 🚀 Deployed preview to | |
| ${{ needs.build.outputs.url }}/pr-preview/pr-${{ matrix.pr_nums }} | |
| ${{ env.DATE }} | |
| " | |
| # Add development URL | |
| development-preview: | |
| needs: [build, deploy] | |
| # If there are open PRs (whose head branch is neither `development` nor `main`), run this job | |
| if: ${{ github.event.pull_request.head.ref == 'development' }} | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Get date | |
| run: echo "DATE=$(date '+%Y-%m-%d %H:%M %Z')" >> $GITHUB_ENV | |
| - name: Add development-preview URL | |
| if: ${{github.event.action != 'closed'}} | |
| uses: thollander/[email protected] | |
| with: | |
| comment_tag: pr-preview | |
| pr_number: ${{ github.event.number }} | |
| message: "\ | |
| Development website preview | |
| :---: | |
| 🚀 Development website deployed to | |
| ${{ needs.build.outputs.url }}/development-website | |
| ${{ env.DATE }} | |
| " | |
| # Change preview message if deployment fails | |
| failed-preview: | |
| needs: deploy | |
| # If the action failed (but was not cancelled) and was fired because of a pull request (not closed) | |
| if: ${{ always() && '!cancelled()' && github.event_name == 'pull_request' && github.event.action != 'closed' && needs.deploy.outputs.success != '1' }} | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Get date | |
| run: echo "DATE=$(date '+%Y-%m-%d %H:%M %Z')" >> $GITHUB_ENV | |
| - name: Change development-preview message | |
| if: ${{ github.event.pull_request.head.ref == 'development' }} | |
| uses: thollander/[email protected] | |
| with: | |
| comment_tag: pr-preview | |
| pr_number: ${{ github.event.number }} | |
| message: "\ | |
| Development website preview | |
| :---: | |
| ⚠️ There was an error in the deployment of the development website. | |
| For more information, please check the [Actions](https://github.com/${{github.repository}}/actions) tab. | |
| ${{ env.DATE }} | |
| " | |
| - name: Change pr-preview message | |
| if: ${{ github.event.pull_request.head.ref != 'development' }} | |
| uses: thollander/[email protected] | |
| with: | |
| comment_tag: pr-preview | |
| pr_number: ${{ github.event.number }} | |
| message: "\ | |
| PR preview | |
| :---: | |
| ⚠️ There was an error in the pr-preview deployment. | |
| For more information, please check the [Actions](https://github.com/${{github.repository}}/actions) tab. | |
| ${{ env.DATE }} | |
| " |