diff options
| author | Sean Whitton <spwhitton@spwhitton.name> | 2022-08-30 19:22:34 -0700 |
|---|---|---|
| committer | Sean Whitton <spwhitton@spwhitton.name> | 2023-05-24 20:30:43 -0700 |
| commit | 5d3a68f8bbaf7f330251441d54e2dcdf47a5df78 (patch) | |
| tree | 460420496080aaaac830890eac4ebffc51f05f8b | |
| parent | d0d972e192f694475d4b722ebd8e1fbb4055b2b0 (diff) | |
| download | dotfiles-5d3a68f8bbaf7f330251441d54e2dcdf47a5df78.tar.gz | |
sync from erebus ~/doc on melete
| -rw-r--r-- | lib-src/mr/config | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/lib-src/mr/config b/lib-src/mr/config index db4a686e..c2e19c70 100644 --- a/lib-src/mr/config +++ b/lib-src/mr/config @@ -229,7 +229,11 @@ checkout = git clone demeterp:doc doc update = git pull --rebase=false --no-edit "$@" autoci = doccheckin pre_update = win32 || doccheckin -sync = doccheckin && git pull --no-edit && git push +sync = + ssh -o ConnectTimeout=3 -o ForwardAgent=yes erebus \ + 'cd $HOME/doc; export PATH=/opt/emacs-snapshot/bin:$PATH; + . $HOME/.profile; doccheckin; git push-all' + doccheckin && git pull --no-edit && git push # Set mtimes to last commit, for Howm; doing so only in post_checkout, and not # fixups, should be sufficient for summary buffer ordering purposes. post_checkout = git utime |