Remove CI files under aux/: remove website from CI

Since I'm already only publishing from my local machine.

1 files changed, 0 insertions, 52 deletions

diff --git a/aux/ci/ci-build.sh b/aux/ci/ci-build.sh
deleted file mode 100755
index b6769a9..0000000
--- a/aux/ci/ci-build.sh
+++ /dev/null
@@ -1,52 +0,0 @@
-#!/bin/sh
-set -eux
-
-PACKAGE="$1"
-LOGS_DIR="$2"
-read -r _ SHA _ # oldrev newrev refname
-FILENAME="$(date -Is)-$SHA.log"
-LOGFILE="$LOGS_DIR/$FILENAME"
-
-{
-	echo "Starting CI job at: $(date -Is)"
-
-	finish() {
-		STATUS="$?"
-		printf "\n\n>>> exit status was %s\n" "$STATUS"
-		echo "Finishing CI job at: $(date -Is)"
-		cd -
-		NOTE=$(cat <<EOF
-See CI logs with:
-	git notes --ref=refs/notes/ci-logs show $SHA
-	git notes --ref=refs/notes/ci-data show $SHA
-EOF
-)
-		git notes --ref=refs/notes/ci-data add -f -m "$STATUS $FILENAME"
-		git notes --ref=refs/notes/ci-logs add -f -F "$LOGFILE"
-		git notes append -m "$NOTE"
-
-		cd -
-		sh aux/ci/report.sh "$PACKAGE"
-		rsync -a public/ "/srv/http/$PACKAGE/" --delete
-
-		printf "\n>>>\n>>> CI logs added as Git note.\n>>>\n>>> Run status was %s" "$STATUS"
-	}
-	trap finish EXIT
-
-	unset GIT_DIR
-	REMOTE="$PWD"
-	cd "$(mktemp -d)"
-	git clone "$REMOTE" .
-	git config --global user.email git@euandre.org
-	git config --global user.name 'EuAndreh CI'
-	git fetch origin refs/notes/*:refs/notes/*
-	git annex get ||:
-
-	if [ -f aux/guix/with-container.sh ]; then
-		RUNNER='./aux/guix/with-container.sh'
-	else
-		RUNNER='sh -c'
-	fi
-
-	$RUNNER 'make clean public dev-check'
-} 2>&1 | tee "$LOGFILE"