diff options
Diffstat (limited to '.github/workflows/ci.yml')
| -rw-r--r-- | .github/workflows/ci.yml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 753872ae1..fd6b65998 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,7 +10,7 @@ jobs: production, production-clang, debug, - debug-cln + debug-cln-clang ] exclude: @@ -18,7 +18,7 @@ jobs: os: macos-latest - name: debug os: macos-latest - - name: debug-cln + - name: debug-cln-clang os: macos-latest include: @@ -43,9 +43,10 @@ jobs: os: ubuntu-latest exclude_regress: 1-4 - - name: debug-cln + - name: debug-cln-clang config: debug --symfpu --cln --gpl --no-debug-symbols --no-proofs --poly - cache-key: debug-cln + cache-key: debug-cln-clang + env: CC=clang CXX=clang++ os: ubuntu-latest exclude_regress: 1-4 |