push-to-public « maint - pciutils/pciutils.git - The PCI Utilities - development tree

about summary refs log tree commit diff stats

path: root/maint/push-to-public

blob: d1ab4f30c801bc763d0677193405d5d33213c974 (plain)

#!/bin/sh
set -e
git push public
git push github