From 783ccf5ee4a79881ee7afb5c9ab33a4f5ce2e851 Mon Sep 17 00:00:00 2001 From: Ilmari Vacklin Date: Tue, 7 Dec 2021 10:00:40 +0200 Subject: [PATCH] Fix Agda module HTML --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index f70adc4..567c313 100644 --- a/Makefile +++ b/Makefile @@ -36,7 +36,7 @@ PANDOC_FLAGS := \ --include-in-header=header.html .PHONY: all -all: $(html_dst) $(js_dst) $(agda_dst) $(styles_dst) $(fonts_dst) +all: $(md_dst) $(html_dst) $(js_dst) $(agda_dst) $(styles_dst) $(fonts_dst) $(OUT_DIR)/%.md: $(SRC_DIR)/%.lagda.md $(AGDA) $(AGDA_FLAGS) $<