diff options
| author | Aleksandr Nogikh <nogikh@google.com> | 2023-05-17 19:23:42 +0200 |
|---|---|---|
| committer | Aleksandr Nogikh <wp32pw@gmail.com> | 2023-05-17 20:35:05 +0200 |
| commit | 3bb7af1def6b7b99e4c1c9573162eb41b5893cd3 (patch) | |
| tree | f3f4ace0042e4f42aa41b71431a660d10a39b7ec /executor/common_ext_example.h | |
| parent | 258520f6c30d9f726364c05921eca9e2015a26cb (diff) | |
dashboard: update HeadReproLevel separately
There are cases when we have revoked a reproducer, but quickly found a
newer one. In that case we should update HeadReproLevel.
Diffstat (limited to 'executor/common_ext_example.h')
0 files changed, 0 insertions, 0 deletions