From 08dc0a8f19a9a30272cfa93f666cd09979e3caa9 Mon Sep 17 00:00:00 2001
From: Konrad 'ktoso' Malawski <ktoso@typesafe.com>
Date: Thu, 22 May 2014 11:51:14 +0200
Subject: [PATCH 1/2] +scr additional functions for tagging issues on github

---
 scripts/build/github-tagging.sh | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100755 scripts/build/github-tagging.sh

diff --git a/scripts/build/github-tagging.sh b/scripts/build/github-tagging.sh
new file mode 100755
index 0000000000..7b24937341
--- /dev/null
+++ b/scripts/build/github-tagging.sh
@@ -0,0 +1,28 @@
+#!/bin/sh
+
+# tag an github issue with the given tag, api token is taken from env ($PR_VALIDATOR_GH_TOKEN)
+# usage: ghtag ISSUE_NR OWNER REPO ADD_TAGS RM_TAGS
+#
+# ADD_TAGS should be json with tokens you want to add, as in: ["tested"]
+# RM_TAGS should be a list of words, like "building bananas"
+function ghtag {
+  if [[ "$PR_VALIDATOR_GH_TOKEN" == "" ]]
+  then
+    echoerr "Env variable PR_VALIDATOR_GH_TOKEN was empty, unable to call github api!"
+    exit 1;
+  fi
+
+  issue=$1
+  owner=$2
+  repo=$3
+  add=$4
+  remove=$5
+
+  curl -H "Authorization: token $PR_VALIDATOR_GH_TOKEN" https://api.github.com/repos/$owner/$repo/issues/$issue/labels -X POST -d $add
+  for d in $remove
+  do
+    curl -H "Authorization: token $PR_VALIDATOR_GH_TOKEN" https://api.github.com/repos/$owner/$repo/issues/$issue/labels/$d -X DELETE
+  done
+}
+
+echoerr() { echo "$@" 1>&2; }

From 9bba4f88fe874674dc7710a94b965dddb9dad8ed Mon Sep 17 00:00:00 2001
From: Konrad 'ktoso' Malawski <ktoso@typesafe.com>
Date: Fri, 23 May 2014 11:12:25 +0200
Subject: [PATCH 2/2] =scr silence curl on jenkins, no need for progress bars

---
 scripts/build/github-tagging.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/scripts/build/github-tagging.sh b/scripts/build/github-tagging.sh
index 7b24937341..306b8ddaa0 100755
--- a/scripts/build/github-tagging.sh
+++ b/scripts/build/github-tagging.sh
@@ -18,10 +18,10 @@ function ghtag {
   add=$4
   remove=$5
 
-  curl -H "Authorization: token $PR_VALIDATOR_GH_TOKEN" https://api.github.com/repos/$owner/$repo/issues/$issue/labels -X POST -d $add
+  curl -s -H "Authorization: token $PR_VALIDATOR_GH_TOKEN" https://api.github.com/repos/$owner/$repo/issues/$issue/labels -X POST -d $add
   for d in $remove
   do
-    curl -H "Authorization: token $PR_VALIDATOR_GH_TOKEN" https://api.github.com/repos/$owner/$repo/issues/$issue/labels/$d -X DELETE
+    curl -s -H "Authorization: token $PR_VALIDATOR_GH_TOKEN" https://api.github.com/repos/$owner/$repo/issues/$issue/labels/$d -X DELETE
   done
 }