diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2020-07-07 10:29:52 +0100 |
---|---|---|
committer | GitHub <[email protected]> | 2020-07-07 10:29:52 +0100 |
commit | 0f5d62a3f3b33edadea50ea93c725ac36460c0d7 (patch) | |
tree | 206a4e526f0991bbccec96b3dc930be884fde93c /docs/dev | |
parent | 0058f97d57d58efe8f97a0e55b1cc83a360cd79c (diff) | |
parent | c88d85bbb497ccf58faf219178ea3cb8b88d3cd5 (diff) | |
parent | 9209a992c9fa8a9421466f8119aa121fee2223e4 (diff) | |
parent | ebdee366b0e16d1d019db2f5c22a730b4451194f (diff) |
Merge #5235 #5236 #5241
5235: Don't ping people in PRs r=matklad a=lnicola
5236: Disable ES module interop r=matklad a=lnicola
5241: Clippy perf warnings r=matklad a=kjeremy
Removes redundant clones
Co-authored-by: Laurențiu Nicola <[email protected]>
Co-authored-by: Aleksey Kladov <[email protected]>
Co-authored-by: kjeremy <[email protected]>