remove extra Makefile command

Galileo-Galilei · Jul 31, 2023 · 4dc97fa · 4dc97fa
1 parent 6dc82c5
commit 4dc97fa
Showing 1 changed file with 0 additions and 3 deletions.
diff --git 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:
-