1 files changed, 0 insertions, 18 deletions
diff --git a/local/triggers/push b/local/triggers/push
deleted file mode 100755
index 7a3cb56..0000000
--- a/local/triggers/push
+++ /dev/null
@@ -1,18 +0,0 @@
-#!/bin/sh
-
-[ "$4" = "W" ] || exit 0
-
-cd "$GL_REPO_BASE/$2.git"
-head=$(git symbolic-ref HEAD)
-
-if ! [ -f "$head" ]; then
-    set -- refs/heads/*
-    if [ "$#" -eq 1 ]; then
-        git symbolic-ref HEAD "$1"
-        echo "NOTICE: Default branch set to $1" >&2
-    else
-        echo "WARNING: The default branch is $head, but no such branch exists" >&2
-    fi
-fi
-
-git log -1 --all --date-order --format=%ci >agefile