Merge remote-tracking branch 'private/dev' into dev

2026-08-29 17:39:02 +02:00 · 2022-11-22 10:42:39 -08:00
parent 207c9ee727 be7c21ab64
commit 6e81ecde54
33 changed files with 387 additions and 234 deletions
@@ -6,6 +6,9 @@ jobs:
    steps:
      - name: Checkout code
        uses: actions/checkout@v1
+      - name: Library build
+        run: |
+         make library
      - name: Docker build
        run: |
         cd ${{ github.workspace }}/docker