star-build

commit 4563ae937aa903af62c4c9a478ee5ea1cf779c93
parent fe9e392cdd465b481eca44767f4ce5de7af2ea9b
Author: Vincent Forest <vincent.forest@meso-star.com>
Date:   Thu,  1 Oct 2026 14:37:08 +0200

noweb: add support for a local mirror

Until this commit noweb script did not allow local mirror of the
repository, and in doing so did not support the installation by being
offline.

Diffstat:
M
src/app-text/noweb.mk.in
 | 
11
++++++++++-

1 file changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/app-text/noweb.mk.in b/src/app-text/noweb.mk.in
@@ -17,7 +17,9 @@
 
 # Configuration macros
 NOWEB_TAG=@TAG@
-NOWEB_URL=https://github.com/nrnrnr/noweb
+NOWEB_URL_ONLINE=https://github.com/nrnrnr/noweb
+NOWEB_URL_OFFLINE=$(MIRROR)/noweb
+NOWEB_URL = $(NOWEB_URL_$(NETWORK))
 
 # Helper macros
 NOWEB_DIR=$(CACHE)/noweb/$(NOWEB_TAG)
@@ -59,6 +61,13 @@ uninstall_noweb: fetch_noweb prefix
 	$(NOWEB_MAKE) uninstall &&\
 	rm -f "$${prefix}/lib/nwmktemp"
 
+mirror_noweb:
+	repo=$(MIRROR)/noweb &&\
+	rm -rf "$${repo}" &&\
+	git clone --bare --branch "$(NOWEB_TAG)" $(MIRROR_GIT_OPT) \
+	  "$(NOWEB_URL)" "$${repo}"
+
 clean_all: clean_noweb
 install_all: noweb
 uninstall_all: uninstall_noweb
+mirror_all: mirror_noweb