delete execution times in docs #21
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: docs | |
| on: | |
| # Manual trigger option in github | |
| # This won't push to github pages where docs are hosted due | |
| # to the gaurded if statement in those steps | |
| workflow_dispatch: | |
| # Trigger on push to these branches | |
| push: | |
| branches: | |
| - main | |
| - version_0.0.1 | |
| # Trigger on a open/push to a PR targeting one of these branches | |
| pull_request: | |
| branches: | |
| - main | |
| - version_0.0.1 | |
| env: | |
| name: Mighty | |
| jobs: | |
| build-and-deploy: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| - name: Setup Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: "3.10" | |
| - name: Install dependencies | |
| run: | | |
| pip install ".[dev,carl,pufferlib]" | |
| - name: Make docs | |
| run: | | |
| make clean | |
| make doc | |
| - name: Pull latest gh-pages | |
| if: (contains(github.ref, 'version_0.2.0') || contains(github.ref, 'main')) && github.event_name == 'push' | |
| run: | | |
| cd .. | |
| git clone https://github.com/${{ github.repository }}.git --branch gh-pages --single-branch gh-pages | |
| - name: Copy new docs into gh-pages | |
| if: (contains(github.ref, 'version_0.2.0') || contains(github.ref, 'main')) && github.event_name == 'push' | |
| run: | | |
| branch_name=${GITHUB_REF##*/} | |
| cd ../gh-pages | |
| rm -rf $branch_name | |
| echo "ls ../${{ env.name }} is: $(ls ../${{ env.name }})" | |
| echo "ls ../${{ env.name }}/docs is: $(ls ../${{ env.name }}/docs)" | |
| echo "ls ../${{ env.name }}/docs/build is: $(ls ../${{ env.name }}/docs/build)" | |
| cp -r ../${{ env.name }}/docs/build/html $branch_name | |
| - name: Push to gh-pages | |
| if: (contains(github.ref, 'version_0.2.0') || contains(github.ref, 'main')) && github.event_name == 'push' | |
| run: | | |
| last_commit=$(git log --pretty=format:"%an: %s") | |
| cd ../gh-pages | |
| branch_name=${GITHUB_REF##*/} | |
| git add $branch_name/ | |
| git config --global user.name 'Github Actions' | |
| git config --global user.email 'not@mail.com' | |
| git remote set-url origin https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/${{ github.repository }} | |
| git commit -am "$last_commit" | |
| git push |