remove obsolete non-jenkins fetch script

diff --git a/fetch b/fetch
deleted file mode 100755 (executable)
index 3a16f88..0000000
--- a/fetch
+++ /dev/null
@@ -1,47 +0,0 @@
-#!/bin/bash
-
-set -e
-
-. ./OPTIONS.sh
-
-scriptname=$1
-shift
-
-if [ -z "$scriptname" ]; then
-    echo "Run with a fetch script as an argument:"
-    (cd fetch-scripts && ls)
-    exit 1
-fi
-
-if ! [ -e fetch-scripts/"$scriptname" ]; then
-    echo "Unknown fetch script $scriptname"
-    exit 1
-fi
-
-mkdir -p "$MIRRORDIR/.locks"
-
-# Save a copy of stdout on FD 3, so we can get it back again
-exec 3>&1
-
-logname="$MIRRORDIR/.logs/$scriptname-$(date +"%F-%R:%S").log"
-
-exec >> "$logname" 2>&1
-date +"Starting $scriptname: %c"
-
-#NB: -r is number of retries, at 8 second intervals
-if lockfile -r 900 "$MIRRORDIR/.locks/$scriptname"; then
-    date +"Received lock: %c"
-    (. fetch-scripts/"$scriptname")
-    exitstatus=$?
-    rm -f "$MIRRORDIR/.locks/$scriptname"
-fi
-
-date +"Done: %c"
-if [ $exitstatus -ne 0 ]; then
-    exec 1>&3 # Restore stdout
-    echo "Synchronization of $scriptname failed:"
-    echo "(last 100 lines)"
-    echo
-    tail -n 100 "$logname"
-fi
-exit $exitstatus