admin-merge: also do a test compile ;)

diff --git a/all b/all
index 7b882074d24bc05df04a93ec89e0049adcba102e..a5e00520bb069eec4cc152ed89745cf0ce98e947 100755 (executable)
--- a/all
+++ b/all
@@ -460,6 +460,9 @@ case "$cmd" in
                        done
                        if [ x"$a" = x"y" ]; then
                                git merge "$1/$2"
+                               cd "$d0"
+                               "$SELF" compile
+                               cd "$d0/d"
                                git push origin HEAD
                                git push "$1" :"$2"
                        fi