aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile5
1 files changed, 4 insertions, 1 deletions
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 = \