From a8cfa7cc9fa9045d13466527793f8baf706a817c Mon Sep 17 00:00:00 2001
From: Paul Andrey <paul.andrey@inria.fr>
Date: Tue, 23 May 2023 16:22:15 +0200
Subject: [PATCH] Remove unused line in 'tox.ini'.

---
 tox.ini | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tox.ini b/tox.ini
index 5977c73a..1e962ca4 100644
--- a/tox.ini
+++ b/tox.ini
@@ -1,6 +1,5 @@
 [tox]
 envlist = py38
-isolated_build = True
 minversion = 3.18.0
 
 [testenv]
-- 
GitLab