Update nightly release script to not duplicate nightlies

This commit is contained in:
Zachary Yedidia
2018-07-20 00:24:02 +00:00
parent 8a250f7d95
commit 1856891622

View File

@@ -1,14 +1,20 @@
# This script creates the nightly release on Github for micro
# You must have the correct Github access token to run this script
commitID=$(git rev-parse HEAD)
info=$(github-release info -u zyedidia -r micro -t nightly)
if [[ $info = *$commitID* ]]; then
echo "No new commits since last nightly"
exit 1
fi
echo "Deleting old release"
github-release delete \
--user zyedidia \
--repo micro \
--tag nightly
commitID=$(git rev-parse HEAD)
echo "Moving tag"
git tag --force nightly $commitID
git push --force --tags