diff options
| author | Sean Whitton <spwhitton@spwhitton.name> | 2018-04-15 21:47:45 -0700 |
|---|---|---|
| committer | Sean Whitton <spwhitton@spwhitton.name> | 2018-04-15 21:47:45 -0700 |
| commit | 7becab25c648e842d32dd340f47425ca8c464794 (patch) | |
| tree | c8f65dbc02c1c2dc254042d82637d24bb4d3506a | |
| parent | c9fc74a3ed6e9b5df904853bdc3f558a774e2dbb (diff) | |
| download | dotfiles-7becab25c648e842d32dd340f47425ca8c464794.tar.gz | |
dummy autoci cmds
| -rw-r--r-- | home-mrconfig | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/home-mrconfig b/home-mrconfig index 3524f898..86463149 100644 --- a/home-mrconfig +++ b/home-mrconfig @@ -432,6 +432,7 @@ push = : diff = : log = : grep = : +autoci = : # --- my personal documents. Override my global update command back # --- to the myrepos default so that git automatically pulls and @@ -481,6 +482,7 @@ fetch = : diff = : log = : grep = : +autoci = : skip = lazy # this is slower than other repos for which sync is defined, so have |