From 65cb5e2bea54a8b9e2de7ad393af08d06e3a2a9f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 29 Mar 2018 14:25:48 +0200 Subject: [PATCH] chore(script/deploy_nightly): show git log --- script/deploy_nightly.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/script/deploy_nightly.sh b/script/deploy_nightly.sh index 63b522c90a..9c4313171c 100644 --- a/script/deploy_nightly.sh +++ b/script/deploy_nightly.sh @@ -24,6 +24,8 @@ then echo -e "Changes since ${last_tag}:\n\n" > diff.md git show $last_tag:doc/changes.md > old.md ./script/diff_changelogs.py old.md doc/changes.md >> diff.md + echo -e "*Full commit log*\n" >> diff.md + git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md git push nightly $LEAN_VERSION_STRING gothub release -s $GH_TOKEN -u leanprover -r lean-nightly -t $LEAN_VERSION_STRING -d - --pre-release < diff.md else