diff options
| -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 |