Fixed gds parse to use type in the textbody as datatype for the gds l… #156
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: github pages | |
| permissions: write-all | |
| on: | |
| push: | |
| branches: | |
| - main # deploy main. If your branch is `master`, you'll have to replace that throughout this file. | |
| pull_request_target: # This will publish a site preview on every pull request, and also run the build command to test if the site is broken. | |
| jobs: | |
| deploy: | |
| runs-on: ubuntu-22.04 | |
| env: | |
| PR_PATH: pull/${{github.event.number}} | |
| steps: | |
| - name: Comment on PR | |
| uses: hasura/[email protected] | |
| if: github.ref != 'refs/heads/main' | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| repository: ${{ github.repository }} | |
| number: ${{ github.event.number }} | |
| id: deploy-preview | |
| message: "Starting deployment of preview ⏳..." | |
| - name: Set domain | |
| run: echo "DOMAIN=lip6.github.io" >> $GITHUB_ENV # TODO set your custom domain | |
| # If you're using the default github pages url, use this instead: | |
| # run: echo "DOMAIN=${{ github.actor }}.github.io" >> $GITHUB_ENV | |
| - name: Checkout website repo | |
| uses: actions/checkout@v2 | |
| with: | |
| submodules: true # fetch the theme | |
| # you need to set this as an environment env if your repo or any submodules (e.g the theme) is private: | |
| # token: ${{ secrets.PRIVATE_REPO_TOKEN }} | |
| - name: Set production base URL | |
| run: echo "BASE_URL=https://${{ env.DOMAIN }}/${{ github.event.repository.name }}/" >> $GITHUB_ENV | |
| - name: Setup PDM | |
| uses: pdm-project/setup-pdm@v3 | |
| - name: Build website | |
| run: | | |
| sudo apt install -y graphviz doxygen doxygen-latex python3-docutils qtbase5-dev libqt5svg5-dev | |
| pdm sync -d --no-self | |
| pdm run meson setup --prefix=/home/runner/work/install -D docs=true -D only-docs=true -D docs-siteurl=$BASE_URL builddir | |
| pdm run meson install -C builddir | |
| - name: Deploy if this is the `main` branch | |
| uses: peaceiris/actions-gh-pages@v3 | |
| if: github.ref == 'refs/heads/main' | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN }} | |
| publish_dir: /home/runner/work/install/share/doc/html | |
| cname: ${{ env.DOMAIN }} # TODO you need to set this if you're using a custom domain. Otherwise you can remove it. | |
| - name: Set base URL for preview if PR | |
| if: github.ref != 'refs/heads/main' | |
| run: echo "BASE_URL=https://${{ env.DOMAIN }}/${{ github.event.repository.name }}/${{ env.PR_PATH}}/" >> $GITHUB_ENV | |
| - name: Build PR preview website | |
| if: github.ref != 'refs/heads/main' | |
| run: | | |
| pdm run meson setup -D docs=true -D docs-siteurl=$BASE_URL builddir | |
| pdm run meson install -C builddir | |
| - name: Deploy to PR preview | |
| uses: peaceiris/actions-gh-pages@v3 | |
| if: github.ref != 'refs/heads/main' | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN }} | |
| publish_dir: /home/runner/work/install/share/doc/html | |
| destination_dir: ${{ env.PR_PATH }} # TODO you need to set this if you're using a custom domain. Otherwise you can remove it. | |
| - name: Update comment | |
| uses: hasura/[email protected] | |
| if: github.ref != 'refs/heads/main' | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| repository: ${{ github.repository }} | |
| number: ${{ github.event.number }} | |
| id: deploy-preview | |
| message: "A preview of ${{ github.event.after }} is uploaded and can be seen here:\n\n ✨ ${{ env.BASE_URL }} ✨\n\nChanges may take a few minutes to propagate. Since this is a preview of production, content with `draft: true` will not be rendered. The source is here: https://github.com/${{ github.repository }}/tree/gh-pages/${{ env.PR_PATH }}/" |