diff options
| author | EuAndreh <eu@euandre.org> | 2023-03-27 09:52:08 -0300 |
|---|---|---|
| committer | EuAndreh <eu@euandre.org> | 2023-03-27 09:52:08 -0300 |
| commit | f5405c44966c6c39fab95f7c9e0e4e7ee4b87120 (patch) | |
| tree | 7c8b7226075983aa8c9fa59122bc835dc4f5696d /Makefile | |
| parent | Use "deployer" as the owner of HTML files (diff) | |
| download | server-f5405c44966c6c39fab95f7c9e0e4e7ee4b87120.tar.gz server-f5405c44966c6c39fab95f7c9e0e4e7ee4b87120.tar.xz | |
Makefile: Add "public/dev/ci" as a dependency of "public"
Notes
See CI logs with:
git notes --ref=refs/notes/ci-logs show f5405c44966c6c39fab95f7c9e0e4e7ee4b87120
git notes --ref=refs/notes/ci-data show f5405c44966c6c39fab95f7c9e0e4e7ee4b87120
Exit status: 0
Duration: 21
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -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 = \ |