diff options
| -rw-r--r-- | home-mrconfig | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/home-mrconfig b/home-mrconfig index 86463149..1db94c2d 100644 --- a/home-mrconfig +++ b/home-mrconfig @@ -432,6 +432,7 @@ push = : diff = : log = : grep = : +isclean = : autoci = : # --- my personal documents. Override my global update command back @@ -483,6 +484,7 @@ diff = : log = : grep = : autoci = : +isclean = : skip = lazy # this is slower than other repos for which sync is defined, so have |