Add make push / scripts/push.sh

Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
This commit is contained in:
2026-10-10 15:50:31 +02:00
co-authored by Claude Sonnet 5.5
parent 4ee0f57ee5
commit 62c958022a
3 changed files with 37 additions and 2 deletions
+5 -1
View File
@@ -3,9 +3,10 @@ export
COMPOSE = docker compose
.PHONY: help fetch build up down logs rebuild drawings drawings-all drawings-one shell-latex remotes
.PHONY: help fetch push build up down logs rebuild drawings drawings-all drawings-one shell-latex remotes
help:
@echo "make push push the three repos (sv), then this one (main); DRY=1 for a dry run"
@echo "make fetch init/update the submodules (scripts/fetch.sh)"
@echo "make build generate the site into ./site-build"
@echo "make up | down start/stop the local web server (http://127.0.0.1:8080)"
@@ -18,6 +19,9 @@ help:
fetch:
./scripts/fetch.sh
push:
./scripts/push.sh $(if $(DRY),--dry-run)
build:
$(COMPOSE) --profile build run --rm build