Pipe in dune.

savonet · Nov 15, 2023 · 54b2a4c · 54b2a4c
1 parent 18767d7
commit 54b2a4c
Show file tree

Hide file tree

Showing 3 changed files with 848 additions and 309 deletions.
diff --git a/doc/Makefile b/doc/Makefile
@@ -6,7 +6,7 @@ all: dune
 test: dune
 	@for i in $(MD); do \
 	echo -n "Compiling $$i... "; \
-	pandoc --filter=pandoc-include --metadata title="bla" --template=template.html $$i -o /tmp/`basename $$i .md`.html; \
+	pandoc $$i -t json | pandoc-include | pandoc -f json --metadata title="bla" --template=template.html -o /tmp/`basename $$i .md`.html; \
 	echo "done"; \
 	done
 	@dune build @doctest