Merge pull request #1 from joneugster/build_executable

fix: build gameserver executable in github action
Trequetrum · Jan 16, 2024 · fac4cd9 · fac4cd9
2 parents 45732fa + 54a284f
commit fac4cd9
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -23,6 +23,7 @@ jobs:
           lean --version
           lake --version
 
+        # Note: this would also happen in the lake post-update-hook
       - name: get mathlib cache
         continue-on-error: true
         run: |
@@ -35,6 +36,10 @@ jobs:
       - name: create timestamp file
         run: touch tmp_timestamp
 
+        # Note: this would also happen in the lake post-update-hook
+      - name: build gameserver executable
+        run: env LEAN_ABORT_ON_PANIC=1 lake build gameserver
+
       - name: building game
         run: env LEAN_ABORT_ON_PANIC=1 lake build