ci: Automatically generate documentation

2022-07-04 06:51:07 +02:00
parent c61e2cb2ce
commit 208fb31040
1 changed files with 88 additions and 0 deletions
@@ -0,0 +1,88 @@
 name: Generate Documentation
 on:
  push:
    branches:
      - '*'
      - '!documentation'
    paths:
      - '.github/workflows/documentation.yml'
      - 'docs/**'
      - 'tools/**'
      - 'LICENSE'
 jobs:
  docs:
    name: "Generate Documentation"
    runs-on: ubuntu-latest
    steps:    
    - name: "Set up Git"
      shell: bash
      run: |
        git config --global user.name 'GitHub Actions'
        git config --global user.email 'xaymar@users.noreply.github.com'
        git config --global pull.ff only
        git config --global pull.rebase true
    - name: "Clone"
      uses: actions/checkout@v3
      with:
        submodules: 'recursive'
        fetch-depth: 0
    - name: "Clone Documentation"
      uses: actions/checkout@v3
      with:      
        ref: 'documentation'
        path: 'build/docs/html'
        submodules: 'recursive'
        fetch-depth: 0
 #        git clone --progress --recursive -b documentation --single-branch https://x-access-token:${{ github.token }}@github.com/${{ github.repository }} "${{ github.workspace }}/build/docs/html"
    - name: "Install Prerequisites"
      shell: bash
      run: |
        sudo apt-get install make python3 python3-pip python3-virtualenv
    - name: "Install Sphinx and Themes into a VirtualEnv"
      shell: bash
      run: |
        source ~/.profile
        virtualenv build/venv
        source build/venv/bin/activate
        pip install sphinx
        pip install sphinx-rtd-theme
    - name: "Generate Documentation"
      shell: bash
      run: |
        source ~/.profile
        source build/venv/bin/activate
        pushd tools
        make html
        ls -lha
        popd
        ls -lha
    - name: "Update Documentation"
      shell: bash
      run: |
        pushd build/docs/html
        git add .
        git --no-pager diff --patch --minimal HEAD --
        git update-index --refresh
        if ! git diff-index --quiet HEAD --; then
          git commit -a -m "${{ github.sha }}"
          # Only push from master branch.
          if [[ "${{ github.ref }}" == "refs/heads/master" ]]; then
            git push
            echo "Documentation has been updated!"
          else
            git log --graph --pretty=format:'%Cred%h%Creset -%C(yellow)%d%Creset %s %Cgreen(%cr) %C(bold blue)<%an>%Creset' --abbrev-commit
          fi
        else
          echo "Documentation is still up to date."
        fi
        popd