From 3b04e8337e5de4ea196c5e8962984d52c9048c0c Mon Sep 17 00:00:00 2001
From: Andreas Zweili <andreas@zweili.ch>
Date: Thu, 13 Jul 2023 22:22:23 +0200
Subject: [PATCH] Remove the .direnv directory when cleaning

---
 dev.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev.sh b/dev.sh
index 433f0cf..0d58129 100755
--- a/dev.sh
+++ b/dev.sh
@@ -54,7 +54,7 @@ clean () {
 
 cleanall () {
     clean
-    rm -r .venv
+    rm -r .venv .direnv/
 }
 
 init () {