From bdbe8f62c00c1e20010dd9cff7c9c9af18d3bb96 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 27 Dec 2024 14:37:15 -0800
Subject: [PATCH] Do not ship _cache and _output for share/

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

diff --git a/Makefile b/Makefile
index 4263ba2b1..15938edad 100644
--- a/Makefile
+++ b/Makefile
@@ -85,8 +85,10 @@ do-install: plugin lib-pulse
 	# Set up fstar.include so users only include lib/pulse
 	echo 'lib' > $(PREFIX)/lib/pulse/fstar.include
 
-	# Install share/ too, as-is.
+	# Install share/ too, as-is, but remove _cache and _output
 	cp -p -t $(PREFIX) -r share/
+	find $(PREFIX)/share/ -path '**/_cache*' -delete
+	find $(PREFIX)/share/ -path '**/_output*' -delete
 
 .PHONY: clean
 clean: