chore(script/deploy_nightly): show git log

leodemoura · Mar 29, 2018 · 65cb5e2 · 65cb5e2
1 parent 56f823b
commit 65cb5e2
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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