From b71a78c8c8466f68c606ffd85b04309d3f5cc963 Mon Sep 17 00:00:00 2001 From: ianshill Date: Thu, 29 Feb 2024 15:08:50 +1100 Subject: [PATCH] Website update ' --- Makefile | 1 - 1 file changed, 1 deletion(-) diff --git a/Makefile b/Makefile index a5746f5..8d86bc8 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,6 @@ EXTRA_DIR:= doc-config COQDOCFLAGS:= \ --toc --toc-depth 2 --html --interpolate \ - -d docs \ --index indexpage --no-lib-name --parse-comments \ --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html export COQDOCFLAGS