add dbginfo to src/Makefile, add building dbginfo example to CI. Fixes #2681, supersedes #2682

2025-06-12 20:53:55 +02:00
parent a8b9c05584
commit 86cf60d0e6
3 changed files with 8 additions and 1 deletions
--- a/.github/workflows/build-on-pull-request.yml
+++ b/.github/workflows/build-on-pull-request.yml
@@ -27,6 +27,9 @@ jobs:
      - name: Build the tools.
        shell: bash
        run: make -j2 bin USER_CFLAGS=-Werror
+      - name: Build the dbginfo example
+        shell: bash
+        run: make -j2 src dbginfo
      - name: Build the utilities.
        shell: bash
        run: make -j2 util