diff options
| author | Oliver Schneider <git-spam-no-reply9815368754983@oli-obk.de> | 2018-02-09 18:53:41 +0100 |
|---|---|---|
| committer | Oliver Schneider <git-spam-no-reply9815368754983@oli-obk.de> | 2018-03-16 18:24:08 +0100 |
| commit | 02ac15cb898a3c74b1bd2453e5ff9fdb35e03157 (patch) | |
| tree | 28a6f2a2d434ebf8d49e92f93a085a2b90ffe5cb /src/tools | |
| parent | 3b6412b94324b10f698a18ea5766ef6ff8921ae8 (diff) | |
Automatically enable the `clippy` feature of `rls` if clippy builds
Diffstat (limited to 'src/tools')
| m--------- | src/tools/clippy | 25 | ||||
| m--------- | src/tools/miri | 36 | ||||
| m--------- | src/tools/rls | 0 |
3 files changed, 37 insertions, 24 deletions
diff --git a/src/tools/clippy b/src/tools/clippy -Subproject d5e233a720495c52af25d8f6dcc9e55e1193beb +Subproject 6f3f25878f2271911e4b6de4d0cf86accc39745 diff --git a/src/tools/miri b/src/tools/miri -Subproject 61833b9aeab8bf8f0c0c0e42b7c96b6eceb37d0 +Subproject d4712ca37500f26bbcbf97edcb27820717f769f diff --git a/src/tools/rls b/src/tools/rls -Subproject b6c52443424977bd92cf7ed127f7771fe9c285d +Subproject fc4db0a5e99e426fd97de370c6f36f585b6af13 |