From 058a4c665e55a8654d253bf9cafaf814b465fbd9 Mon Sep 17 00:00:00 2001
From: Amber Brown <hawkowl@atleastfornow.net>
Date: Wed, 3 Oct 2018 00:59:11 +1000
Subject: Remove Jenkins & other old dev junk (#3988)

---
 jenkins/clone.sh | 44 --------------------------------------------
 1 file changed, 44 deletions(-)
 delete mode 100755 jenkins/clone.sh

(limited to 'jenkins')

diff --git a/jenkins/clone.sh b/jenkins/clone.sh
deleted file mode 100755
index ab30ac7782..0000000000
--- a/jenkins/clone.sh
+++ /dev/null
@@ -1,44 +0,0 @@
-#! /bin/bash
-
-# This clones a project from github into a named subdirectory
-# If the project has a branch with the same name as this branch
-# then it will checkout that branch after cloning.
-# Otherwise it will checkout "origin/develop."
-# The first argument is the name of the directory to checkout
-# the branch into.
-# The second argument is the URL of the remote repository to checkout.
-# Usually something like https://github.com/matrix-org/sytest.git
-
-set -eux
-
-NAME=$1
-PROJECT=$2
-BASE=".$NAME-base"
-
-# Update our mirror.
-if [ ! -d ".$NAME-base" ]; then
-  # Create a local mirror of the source repository.
-  # This saves us from having to download the entire repository
-  # when this script is next run.
-  git clone "$PROJECT" "$BASE" --mirror
-else
-  # Fetch any updates from the source repository.
-  (cd "$BASE"; git fetch -p)
-fi
-
-# Remove the existing repository so that we have a clean copy
-rm -rf "$NAME"
-# Cloning with --shared means that we will share portions of the
-# .git directory with our local mirror.
-git clone "$BASE" "$NAME" --shared
-
-# Jenkins may have supplied us with the name of the branch in the
-# environment. Otherwise we will have to guess based on the current
-# commit.
-: ${GIT_BRANCH:="origin/$(git rev-parse --abbrev-ref HEAD)"}
-cd "$NAME"
-# check out the relevant branch
-git checkout "${GIT_BRANCH}" || (
-    echo >&2 "No ref ${GIT_BRANCH} found, falling back to develop"
-    git checkout "origin/develop"
-)
-- 
cgit 1.4.1