Merge remote-tracking branch 'origin/fix_2050'

MarkBind · Nov 27, 2023 · 8b94e7a · 8b94e7a
2 parents 1910332 + 4f41883
commit 8b94e7a
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 5 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -88,10 +88,17 @@ jobs:
       - name: Deploy DG on any commit to master, to markbind.org/devdocs
         run: >-
           npm run build:web &&
-          npm run build:dg &&
           npm run deploy:dg
       - name: Deploy UG on release, to markbind.org
         if: github.ref_type == 'tag'
-        run: >-
-          npm run build:ug &&
-          npm run deploy:ug
+        run: npm run deploy:ug
+      - name: Check deploy log
+        run: |
+          log_file="docs/_markbind/logs/markbind-$(date +'%Y-%m-%d').log"
+          pattern="^[0-9T:.Z-]+ - error:"
+          
+          if grep -q -E "$pattern" "$log_file"; then
+            printf "The following issues were found when deploying the documentation:\n"
+            grep -E "$pattern" "$log_file"
+            exit 1
+          fi
diff --git a/docs/devGuide/projectManagement.md b/docs/devGuide/projectManagement.md
@@ -199,7 +199,6 @@ For general best practices, refer to the guide [_Working with PRs_ @SE-EDU](http
    The deployment is automated. However, if it doesn't deploy properly for the release, do the following:
 
    ```sh
-   $ npm run build:ug
    $ npm run deploy:ug
    ```
-Original file line number
+Diff line change
@@ Expand Up @@
        The deployment is automated. However, if it doesn't deploy properly for the release, do the following:
        ```sh
-       $ npm run build:ug
        $ npm run deploy:ug
        ```
@@ Expand Down @@