diff options
author | stuebinm | 2022-04-04 00:11:39 +0200 |
---|---|---|
committer | stuebinm | 2022-04-04 00:11:39 +0200 |
commit | f08c3dbfd38ed4a1195cf36a813eb84c4ccbf4f0 (patch) | |
tree | 29b36309f0cdc2194dd75618677bb0ad40bbcd1a | |
parent | 7e9941bf90644120b3627d0f0f66204fed9efb2a (diff) |
server: actually use git repository updates
before this, the server would fetch updates but then not update the
corresponding reference, leading to the initial state being checked out
and linted again.
-rw-r--r-- | server/Worker.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/server/Worker.hs b/server/Worker.hs index 31ddcdc..a9ffce3 100644 --- a/server/Worker.hs +++ b/server/Worker.hs @@ -93,7 +93,7 @@ runJob offline config Job {..} done = do True | offline -> logInfoN $ "offline mode: not updating " <> show gitdir | otherwise -> (liftIO $ callgit gitdir - [ "fetch", "origin", toString ref, "--depth", "1" ]) + [ "fetch", "origin", toString (ref <> ":" <> ref) ]) rev <- map T.strip -- git returns a newline here $ readgit' gitdir ["rev-parse", toString ref] |