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 | |
| 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.
| -rw-r--r-- | .envrc | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -53,6 +53,8 @@ git config --local branchless.test.alias.lint 'export CI=1; git clean -ffdx; eval $(direnv export bash); bild Omni/Lint.hs; lint **/*' git config --local branchless.test.alias.lintfix 'export CI=1; git clean -ffdx; eval $(direnv export bash); bild Omni/Lint.hs; lint --fix **/*' git config --local branchless.test.alias.ci 'export CI=1; git clean -ffdx; eval $(direnv export bash); Omni/Ci.sh' +# use this to submit work + git config --local alias.live "push origin HEAD:live" # # end here if we are in CI [[ -n "CI" ]] && exit 0 |