fix: Add documentation build (#47)

limakzi · Aug 27, 2024 · 955883c · 955883c
1 parent 1ed7819
commit 955883c
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/.github/workflows/page-update.yaml b/.github/workflows/page-update.yaml
@@ -31,12 +31,18 @@ jobs:
       - name: git -- checkout page
         uses: actions/checkout@v4
         with:
-          path: smallantimagma
+          path: smallantimagmas
           ref: ${{ github.ref_name }}
 
+      - name: metadata -- build docs
+        working-directory: ./smallantimagmas
+        run: |
+          gap makedoc.g
+
       - name: metadata -- copy metada to update page
         run: |
-          cp smallantimagma/PackageInfo.g gh-pages/PackageInfo.g
+          cp smallantimagmas/PackageInfo.g gh-pages/PackageInfo.g
+          cp -r smallantimagmas/doc/ gh-pages/doc/
 
       - name: metadata -- update page
         working-directory: ./gh-pages