diff options
| author | Ben Sima <ben@bsima.me> | 2024-12-21 14:19:42 -0500 |
|---|---|---|
| committer | Ben Sima <ben@bsima.me> | 2024-12-21 14:19:42 -0500 |
| commit | 27904066fd204a2b844c27132e86f83acf217eed (patch) | |
| tree | 61d276c7a1c1eb4722f579a5488e9e3670a7b4e0 /Omni/Cli.hs | |
| parent | 70543fc1ef9733fb754cecda96805349cb36de32 (diff) | |
This is the correct way to publish commits. Previously I was doing the annoying
`git branch -f live HEAD && git push` thing. This is better because its a single
command and doing the subsequent `git sync -u` will update your local `live`
branch.
Diffstat (limited to 'Omni/Cli.hs')
0 files changed, 0 insertions, 0 deletions