From c5fe3e659e047c74eefdd72c8d71bea345dc62c1 Mon Sep 17 00:00:00 2001
From: Ilmari Vacklin <ilmari.vacklin@iki.fi>
Date: Fri, 12 Aug 2022 12:17:14 +0000
Subject: [PATCH] ignore .direnv

---
 .gitignore | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 8794f3b..6bf4d8f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 *.agdai
 /_build/
-/html/.direnv/
+/html/
+.direnv/