From f5405c44966c6c39fab95f7c9e0e4e7ee4b87120 Mon Sep 17 00:00:00 2001 From: EuAndreh Date: Mon, 27 Mar 2023 09:52:08 -0300 Subject: Makefile: Add "public/dev/ci" as a dependency of "public" --- Makefile | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 708b1a0..7abb4bc 100644 --- a/Makefile +++ b/Makefile @@ -65,8 +65,11 @@ public/index.html: README.md $(html-deps) public/TODOs.html: TODOs.md $(html-deps) td -H | sh doc/md2html.sh -T 'TODOs' > $@ +public/dev/ci: + sh src/infrastructure/scripts/report.sh -o $@ + public: \ - public/index.html public/TODOs.html + public/index.html public/TODOs.html public/dev/ci prod-secrets.txt.gpg = \ -- cgit v1.2.3