Skip to content

Commit

Permalink
Slightly better describe-system-config
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Nov 11, 2023
1 parent 5200386 commit 2b0b55c
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/coq-debian.yml
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ jobs:
run: etc/ci/describe-system-config.sh
- name: chroot build params
shell: in-debian-chroot.sh {0}
run: etc/ci/describe-system-config.sh
run: CI=1 etc/ci/describe-system-config.sh
- name: make deps
shell: in-debian-chroot.sh {0}
run: etc/ci/github-actions-make.sh -j2 deps
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/coq-windows.yml
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ jobs:
shell: cmd

- name: echo build params
run: etc/ci/describe-system-config-win.bat
run: ./etc/ci/describe-system-config-win.bat
shell: cmd
- name: deps
run: |
Expand Down

0 comments on commit 2b0b55c

Please sign in to comment.