From 2112e7c8b72bdf1c3bf1577326c4850fa8d2b265 Mon Sep 17 00:00:00 2001
From: Adrien Abraham <adrien.abraham@insectes.org>
Date: Fri, 30 Jun 2023 12:03:25 +0200
Subject: [PATCH] setup-python-dev-tools: remove script

---
 setup-python-dev-tools.sh | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100755 setup-python-dev-tools.sh

diff --git a/setup-python-dev-tools.sh b/setup-python-dev-tools.sh
deleted file mode 100755
index 8bd5d91..0000000
--- a/setup-python-dev-tools.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/bash
-
-ask_install() {
-    packages="$@"
-    read -p "Install $packages? [y/n] " -n 1 -r ; echo
-    [[ "$REPLY" = y ]] && pip3 install $packages
-}
-
-ask_install jedi-language-server
-ask_install pycodestyle
-ask_install pylint
-ask_install mypy