diff options
| -rw-r--r-- | home-mrconfig | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/home-mrconfig b/home-mrconfig index 711b5566..1945de70 100644 --- a/home-mrconfig +++ b/home-mrconfig @@ -443,7 +443,7 @@ skip = ! mine #fixups = git-utime # before pulling, automatically commit in the same way that my cron job does -pre_update = (! win32) && doccheckin +pre_update = win32 || doccheckin # ... and let me do it manually autoci = doccheckin || true |