Re-remove util/dev

Maybe someday, git subtree will do it right
2020-05-17 01:14:28 +02:00
parent cb0d40a7ec
commit 404ae5b211
1 changed files with 0 additions and 7 deletions
--- a/util/dev
+++ b/util/dev
@@ -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 -- "$@"