max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: CI: ignore diff exit code

Browse source
This commit is contained in:
Sebastian Ullrich 2022-02-13 00:04:08 +01:00
parent 8be916b0cf
commit 340c331da9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View file

@ -235,7 +235,7 @@ jobs:
echo -e "*Changes since ${last_tag}:*\n\n" > diff.md
git show $last_tag:RELEASES.md > old.md
#./script/diff_changelogs.py old.md doc/changes.md >> diff.md
diff --changed-group-format='%>' --unchanged-group-format='' old.md RELEASES.md >> diff.md
diff --changed-group-format='%>' --unchanged-group-format='' old.md RELEASES.md >> diff.md || true
echo -e "\n*Full commit log*\n" >> diff.md
git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
- name: Release Nightly