Update nightly release script to not duplicate nightlies

diff --git a/tools/nightly-release.sh b/tools/nightly-release.sh
index e5360756be7fcdaeb862e60caee62d0c8058d855..372027a546d03333a31961c8c8435c0a8dcb1876 100755 (executable)
--- a/tools/nightly-release.sh
+++ b/tools/nightly-release.sh
@@ -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