Try to FIX CI

Internal-tag: [#58500] Signed-off-by: Robert Winkler <[email protected]>
antmicro · Jul 22, 2024 · 76d2593 · 76d2593
1 parent 9bbf5b2
commit 76d2593
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 35 deletions.
diff --git a/.github/scripts/ci.sh b/.github/scripts/ci.sh
@@ -136,15 +136,14 @@ generate_examples() {
 
 
 generate_docs() {
-    begin_command_group "requirements for doc generation"
     install_common_system_packages
-    install_pyenv
-    log_cmd apt-get install -y texlive-full
-    log_cmd pip install .
-    log_cmd pip install -r "docs/requirements.txt"
+    begin_command_group "Install system packages for doc generation"
+    log_cmd apt-get install -y texlive-full make
+    enter_venv
+
+    begin_command_group "Install python packages for doc generation"
     log_cmd pip install nox
     end_command_group
-    enter_venv
 
     begin_command_group "generating documentation"
     echo -en "\nhtml_js_files = [ '$ANNOTANT', ]" >> docs/source/conf.py

diff --git a/.github/workflows/ghpages.yml b/.github/workflows/ghpages.yml
@@ -12,32 +12,32 @@ jobs:
       image: debian:bookworm
 
     steps:
-    - uses: actions/checkout@v3
-
-    - name: Set up Python 3.9
-      uses: actions/setup-python@v4
-      with:
-        python-version: 3.9
-
-    - name: Generate documentation
-      run: |
-        ./.github/scripts/ci.sh docs
-
-    - uses: actions/upload-artifact@v3
-      with:
-        name: gh-page
-        path: docs/build/html
-
-    - name: Deploy to Github Pages
-      if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request'
-      run: |
-        cd docs/build/html
-        touch .nojekyll
-        git init
-        cp ../../../.git/config ./.git/config
-        git add .
-        git config --local user.email "push@gha"
-        git config --local user.name "GHA"
-        git commit -am "update ${{ github.sha }}"
-        git push -u origin +HEAD:gh-pages
-        rm -rf .git
+      - name: Install git package
+        run: |
+          apt-get update -qq
+          apt-get install -y git
+
+      - uses: actions/checkout@v4
+
+      - name: Generate documentation
+        run: |
+          ./.github/scripts/ci.sh docs
+
+      - uses: actions/upload-artifact@v3
+        with:
+          name: gh-page
+          path: docs/build/html
+
+      - name: Deploy to Github Pages
+        if: github.ref == 'refs/heads/main' && github.event_name != 'pull_request'
+        run: |
+          cd docs/build/html
+          touch .nojekyll
+          git init
+          cp ../../../.git/config ./.git/config
+          git add .
+          git config --local user.email "push@gha"
+          git config --local user.name "GHA"
+          git commit -am "update ${{ github.sha }}"
+          git push -u origin +HEAD:gh-pages
+          rm -rf .git