From 4dc97fad759f13d00ea5bcba86e5eee7d9c6cd35 Mon Sep 17 00:00:00 2001 From: Nok Date: Mon, 31 Jul 2023 19:23:19 +0000 Subject: [PATCH] remove extra Makefile command --- docs/Makefile | 3 --- 1 file changed, 3 deletions(-) diff --git a/docs/Makefile b/docs/Makefile index dad4594..d4bb2cb 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -18,6 +18,3 @@ help: # "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). %: Makefile @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) - -lint: - \ No newline at end of file