diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2020-08-09 22:23:20 +0100 |
---|---|---|
committer | GitHub <[email protected]> | 2020-08-09 22:23:20 +0100 |
commit | 9995e79cce548d43505d91653e2a1fdde8729134 (patch) | |
tree | 74ddb1fbcad761ff7cf2d61683182c321a5f9bbf /.gitignore | |
parent | 859963b9a712817a486088997b23583467cf4958 (diff) | |
parent | 85d5ed367579fb9e868517be0f0df636f6277363 (diff) |
Merge #5414
5414: Fix test code lens r=jonas-schievink a=avrong
Closes #5217
The implementation is quite similar to #4821. Maybe we should somehow deal with duplicated code.
Also, both of these requests introduce some unclear behavior. I'm not sure how to process this, therefore asking for advice. Examples are below.
<img width="286" alt="image" src="https://user-images.githubusercontent.com/6342851/87713209-83595f80-c7b2-11ea-8c0f-a12e7571e7df.png">
Co-authored-by: Aleksei Trifonov <[email protected]>
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions