From 1856891622af0e4616288df6207451553622d465 Mon Sep 17 00:00:00 2001
From: Zachary Yedidia <zyedidia@gmail.com>
Date: Fri, 20 Jul 2018 00:24:02 +0000
Subject: [PATCH] Update nightly release script to not duplicate nightlies

---
 tools/nightly-release.sh | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/tools/nightly-release.sh b/tools/nightly-release.sh
index e5360756b..372027a54 100755
--- 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