summaryrefslogtreecommitdiffstats
path: root/maint/push-to-public
blob: d1ab4f30c801bc763d0677193405d5d33213c974 (plain)
1
2
3
4
#!/bin/sh
set -e
git push public
git push github