#!/bin/bash
# push-public
#
# Push changes to everything local that can be exported to the public
# web server.

git-push-public $*
repo-push-public $*