From 7eb71c136188859dffe038aeabcc9a706e090be7 Mon Sep 17 00:00:00 2001
From: Felix Van der Jeugt <felix.vanderjeugt@posteo.net>
Date: Sat, 14 Nov 2020 14:43:46 +0100
Subject: [PATCH] add script to fetch subgit repos

---
 local/bin/subgit-fetch | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100755 local/bin/subgit-fetch

diff --git a/local/bin/subgit-fetch b/local/bin/subgit-fetch
new file mode 100755
index 0000000..33cb266
--- /dev/null
+++ b/local/bin/subgit-fetch
@@ -0,0 +1,37 @@
+#!/bin/sh
+
+task="$1"
+repo="$2"
+
+set -e
+
+if [ ! -d "$repo" ]; then
+	mkdir -p "$repo"
+	cd "$repo"
+	git init
+else
+	cd "$repo"
+fi
+
+if [ ! -z "$(git status --porcelain)" ]; then
+	echo "Requires a clean working tree" >&2
+	exit 1
+fi
+
+# update existing submodules
+git submodule foreach git fetch origin
+git submodule foreach git reset --hard origin/master
+
+for remote in $(ssh git@subgit.ugent.be task students -l "$task" | cut -f4); do
+	if [ -d "$(basename "$remote")" ]; then
+		true # exists
+	elif [ -z "$(git ls-remote "$remote")" ]; then
+		echo "No branches at $remote"
+	else
+		echo "adding $remote"
+		git submodule --quiet add "$remote"
+	fi
+done
+
+git add .
+git commit -v