Reclaim some storage space to build docs

.github/workflows/build_docs.yml

@@ -30,15 +30,25 @@ name: deploy_dev_docs
 
 on:
   push:
-    branches:
-      - develop
 
 jobs:
   build_docs:
     name: build_dev_docs
     runs-on: ubuntu-latest
 
     steps:
+
+      # Maximize the space in this image
+      - name: Maximize build space
+        uses: easimon/maximize-build-space@master
+        with:
+          root-reserve-mb: 30720
+          remove-dotnet: true
+          remove-android: true
+          remove-haskell: true
+          remove-codeql: true
+          remove-docker-images: true
+
       - uses: actions/checkout@v4
         with:
           fetch-depth: 0 # otherwise, there would be errors pushing refs to the destination repository.
@@ -58,15 +68,15 @@ jobs:
       - name: Build documentation with docker
         run: make docks
 
-      - name: Commit files
-        run: |
-          git add -Af
-          git config --local user.email "[email protected]"
-          git config --local user.name "GitHub Action"
-          git commit -m "Update develop documentation"
-
-      - uses: ad-m/[email protected]
-        with:
-          github_token: ${{ secrets.GITHUB_TOKEN }}
-          branch: doc
-          force: true
+#      - name: Commit files
+#        run: |
+#          git add -Af
+#          git config --local user.email "[email protected]"
+#          git config --local user.name "GitHub Action"
+#          git commit -m "Update develop documentation"
+#
+#      - uses: ad-m/[email protected]
+#        with:
+#          github_token: ${{ secrets.GITHUB_TOKEN }}
+#          branch: doc
+#          force: true