From 0da7f66aa6a2eb133e08250988c92e0aa7346700 Mon Sep 17 00:00:00 2001
From: "Peter J. Holzer" <hjp@hjp.at>
Date: Sat, 22 Oct 2022 22:40:46 +0200
Subject: [PATCH] poll a git repo and invoke make if something changed

---
 pull-and-make | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100755 pull-and-make

diff --git a/pull-and-make b/pull-and-make
new file mode 100755
index 0000000..39b7265
--- /dev/null
+++ b/pull-and-make
@@ -0,0 +1,19 @@
+#!/bin/sh
+#
+# Usage: pull-and-make directory [make-params]
+#
+# This script is intended to continually poll a git repo
+# It will chdir to its first argument and pull from the remote repo
+# If there is a new version it will invoke make with the rest of the
+# arguments
+set -x
+set -e
+cd "$1"
+shift
+git pull > ~/tmp/pull-and-make.$$
+if grep '^Already up to date.$' ~/tmp/pull-and-make.$$
+then
+    exit 1
+fi
+
+make "$@"