From 8d596ea01c6fb90ca254d30cea4b3285d6b415ba Mon Sep 17 00:00:00 2001
From: Philipp Hansch <dev@phansch.net>
Date: Sun, 26 Apr 2020 14:00:03 +0200
Subject: [PATCH] Remove util/dev script

`cargo dev` has been the replacement for a while, so I think we can
remove it now.

cc #5394
---
 util/dev | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100755 util/dev

diff --git a/util/dev b/util/dev
deleted file mode 100755
index 319de217e..000000000
--- a/util/dev
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/sh
-CARGO_TARGET_DIR=$(pwd)/target/
-export CARGO_TARGET_DIR
-
-echo 'Deprecated! `util/dev` usage is deprecated, please use `cargo dev` instead.'
-
-cd clippy_dev && cargo run -- "$@"