Merge remote-tracking branch 'github/master'

1 files changed, 0 insertions, 20 deletions

diff --git a/krebs/5pkgs/simple/Reaktor/scripts/random-issue.sh b/krebs/5pkgs/simple/Reaktor/scripts/random-issue.sh
deleted file mode 100755
index 5c47c6156..000000000
--- a/krebs/5pkgs/simple/Reaktor/scripts/random-issue.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#! /bin/sh
-set -eu
-# requires env:
-#   $state_dir
-#   $origin
-
-# in PATH: git,lentil,coreutils
-subdir=`echo "$1" | tr -dc "[:alnum:]"`
-name=`echo "$origin" | tr -dc "[:alnum:]"`
-track="$state_dir/$name-checkout"
-(if test -e "$track" ;then
-  cd "$track"
-  git fetch origin master
-  git reset --hard origin/master
-else
-  git clone "$origin" "$track"
-fi) >&2
-
-cd "$track"
-lentil "${subdir:-.}" -f csv | sed 1d | shuf | head -1