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 /.gitignore | |
| 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