From 27904066fd204a2b844c27132e86f83acf217eed Mon Sep 17 00:00:00 2001 From: Ben Sima Date: Sat, 21 Dec 2024 14:19:42 -0500 Subject: Add a 'git live' command alias 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. --- .envrc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.envrc b/.envrc index ac0f498..c25bd04 100644 --- a/.envrc +++ b/.envrc @@ -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 -- cgit v1.2.3