#!/bin/bash
# Called once after update, with list of refs pushed in the arguments.

# Files to search for a post-deployment make target
PD_FILES="Makefile .depends.make depends.make site/depends.make config.make .config.make"

for ref in $*; do
    if [ "$ref" = refs/heads/master ]; then
	unset GIT_DIR; export GIT_DIR
	repo=`pwd`
	name=`basename $repo .git`
	# This works because the .../vv and .../git trees have the same layout
	dest=`dirname $repo | sed -e 's/git/vv/'`/$name
	if [ -d $dest ]; then (cd $dest
	    echo Deploying master to $dest from $repo
	    git pull --ff-only # was $repo master, but hopefully origin is configured
	    git update-server-info
	    if grep -qs post-deployment: $PD_FILES; then
		make post-deployment
	    fi
	    )
	else 
	    echo Not deploying because $dest does not exist.
	fi
    else
        echo "Ref $ref received."
    fi
done