update

#!/bin/sh
set -e

exec 2>&1
echo "update script"

# repository url prefix:
REPOSRC=http://github.com/PLRI

# variables pointing to directories
PROJECT_WEB=/home/project-web/arden2bytecode
REPO=$PROJECT_WEB/arden2bytecode-homepage
TARGET_HTDOCS=$PROJECT_WEB/htdocs

# set up git path
PATH=/home/project-web/arden2bytecode/git/bin:$PATH


# cd to repository
cd $REPO
echo "repository is in $(pwd)"
echo "using git binary in $(which git)"

# uncomment these lines if it is the first time you are 
# running this script:
#cd $PROJECT_WEB
#git clone $REPOSRC/arden2bytecode-homepage.git
#cd $REPO
#git submodule update --init

# pull recent version
git pull
git submodule foreach git pull origin master

# generate developer documentation, see makedocs script for more information
if [ -x $REPO/makedocs ]; then
    $REPO/makedocs $REPO/htdocs/includes/developerdocs.html
fi

# copy files to htdocs but exclude all .git directories
rm -rf $TARGET_HTDOCS
rsync -r --exclude='.git' $REPO/htdocs $PROJECT_WEB/

# for your information
echo "done"