diff options
| -rw-r--r-- | common/microlog/2026-09-08.gmi | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/common/microlog/2026-09-08.gmi b/common/microlog/2026-09-08.gmi index 7ef1b45..ee58e79 100644 --- a/common/microlog/2026-09-08.gmi +++ b/common/microlog/2026-09-08.gmi @@ -11,7 +11,7 @@ echo "pushing changes to https://joeac.net and gemini://joeac.net" ssh <user>@<http_machine> 'git -C <dir> pull; make -C <dir>/gemini' git -C <dir> pull make -C <dir>/gemini -) 2>> $log 1>&2 +) 2>> $log 1>&2 & ``` A few tricks: @@ -21,3 +21,4 @@ A few tricks: * make sure `nginx` has a public key stored in the remote user's `~/.ssh/authorized_keys` file * any output to stdout or stderr goes back to the git-pusher's CLI * I've used a sub-shell and redirects to put logs in a logfile and not return them to the git-pusher +* I've also used the ampersand `&` operator so the git-pusher isn't hanging around waiting for the build to finish |