#!/bin/bash
while read OLD_REV NEW_REV REF_NAME; do
  git push -f public $NEW_REV:$REF_NAME
done