From d9267202c2ed7597bd20ba97d117d51e38f8d4e1 Mon Sep 17 00:00:00 2001
From: Ezio Melotti <ezio.melotti@gmail.com>
Date: Mon, 9 Oct 2023 16:12:45 +0200
Subject: [PATCH] Remove unused `SPHINXLINT` var.

---
 Doc/Makefile | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Doc/Makefile b/Doc/Makefile
index 22691895068fea..78ee4271e25f79 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -7,7 +7,6 @@
 PYTHON       = python3
 VENVDIR      = ./venv
 SPHINXBUILD  = PATH=$(VENVDIR)/bin:$$PATH sphinx-build
-SPHINXLINT   = PATH=$(VENVDIR)/bin:$$PATH sphinx-lint
 BLURB        = PATH=$(VENVDIR)/bin:$$PATH blurb
 JOBS         = auto
 PAPER        =