From 4a41d2d6c6134757cd6efea0e6cce48daf77f56d Mon Sep 17 00:00:00 2001
From: Dan Gohman <sunfish@mozilla.com>
Date: Tue, 30 Oct 2018 13:04:21 -0700
Subject: [PATCH] Delete obsolete clippy scripts.

---
 check-clippy.sh | 10 ----------
 1 file changed, 10 deletions(-)
 delete mode 100755 check-clippy.sh

diff --git a/check-clippy.sh b/check-clippy.sh
deleted file mode 100755
index 072069cb9b..0000000000
--- a/check-clippy.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/bin/bash
-set -euo pipefail
-
-# Usage: check-clippy.sh
-
-if cargo install --list | tee /dev/null | grep -q "^clippy v0"; then
-    exit 0
-else
-    exit 1
-fi