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 /server/Main.hs | |
| 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.
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions