diff options
author | stuebinm | 2022-03-20 19:02:06 +0100 |
---|---|---|
committer | stuebinm | 2022-03-20 19:02:06 +0100 |
commit | f72855ea8ade8f94474618c5dacda8dd30171740 (patch) | |
tree | 4f307cd839ade66250ef4e15128976320c2ae7e9 /lib/CheckDir.hs | |
parent | 0032307c5868d56490ac1d968c986f8bab5a637b (diff) |
server: keep (one) last good result per repo
(i.e. we want to still have a valid version of the map if new results
where introduced)
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions