From aec64681eb6993a97da40ca9a949e91ac05b3952 Mon Sep 17 00:00:00 2001 From: Philippe Pittoli Date: Fri, 16 Feb 2024 02:36:48 +0100 Subject: [PATCH] Quick fix to generate the documentation. --- makefile | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/makefile b/makefile index f809951..555fda2 100644 --- a/makefile +++ b/makefile @@ -16,12 +16,15 @@ repl: spagobuild: spago build -docs: +docs-with-search: spago docs +docs: + spago docs --no-search + DOCS_HTTPD_ACCESS_LOGS ?= /tmp/docs-access.log DOCS_HTTPD_ADDR ?= 127.0.0.1 -DOCS_HTTPD_PORT ?= 30000 +DOCS_HTTPD_PORT ?= 31000 DOCS_DIR ?= generated-docs/html serve-docs: docs darkhttpd $(DOCS_DIR) --addr $(DOCS_HTTPD_ADDR) --port $(DOCS_HTTPD_PORT) --log $(DOCS_HTTPD_ACCESS_LOGS)