add update script
authorMichael Wallner <mike@php.net>
Fri, 8 Mar 2019 10:39:20 +0000 (11:39 +0100)
committerMichael Wallner <mike@php.net>
Fri, 8 Mar 2019 10:39:20 +0000 (11:39 +0100)
update.sh [new file with mode: 0755]

diff --git a/update.sh b/update.sh
new file mode 100755 (executable)
index 0000000..9b427f4
--- /dev/null
+++ b/update.sh
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+# pull the app and all refs
+git submodule foreach "git pull -qr origin master"
+
+cd refs
+for ref in http pq; do 
+       ../mdref/bin/ref2stub $ref >/dev/null
+
+       # this is semantically awful
+       if ! diff -q {,$ref/}$ref.stub.php; then
+               cp {,$ref/}$ref.stub.php
+               (cd $ref && git commit -am "update live stub" && git push)
+       fi
+done
+cd ..