Skip to content

Commit

Permalink
Fix Agda module HTML
Browse files Browse the repository at this point in the history
  • Loading branch information
wolverian committed Dec 7, 2021
1 parent 19c6b63 commit 783ccf5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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) $<
Expand Down

0 comments on commit 783ccf5

Please sign in to comment.