From 4eff8b258b1e9bc64f3d831ae160ac9256bfdd79 Mon Sep 17 00:00:00 2001
From: "Lance R. Vick" <lance@lrvick.net>
Date: Thu, 27 Apr 2023 13:54:27 -0700
Subject: [PATCH] optional PRESERVE_CACHE argument

---
 Makefile | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index e724643..6a1f0cb 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,7 @@ UID := $(shell id -u)
 GID := $(shell id -g)
 USER := $(UID):$(GID)
 CPUS := $(shell docker run -it debian nproc)
+PRESERVE_CACHE := "false"
 GIT_REF := $(shell git log -1 --format=%H)
 GIT_AUTHOR := $(shell git log -1 --format=%an)
 GIT_KEY := $(shell git log -1 --format=%GP)
@@ -106,7 +107,8 @@ reproduce: toolchain-clean
 .PHONY: $(DIST_DIR)
 $(DIST_DIR):
 	rm -rf $@/*
-	$(MAKE) toolchain-clean default
+	[ "$(PRESERVE_CACHE)" = "true" ] || $(MAKE) toolchain-clean
+	$(MAKE) default
 	cp -R $(OUT_DIR)/* $@/
 
 $(BIN_DIR):