diff --git a/Makefile b/Makefile
index 79b3720..ad2d172 100644
--- a/Makefile
+++ b/Makefile
@@ -15,10 +15,13 @@ install: $(COQMAKEFILE)
 uninstall: $(COQMAKEFILE)
 	$(MAKE) -f $(COQMAKEFILE) uninstall
 
+export:
+	git archive --output supplementary.tar master --prefix supplementary/source/
+
 theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig
 	autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig
 
-.PHONY: clean FORCE
+.PHONY: clean FORCE export
 
 clean:
 	test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) )
diff --git a/README.org b/README.org
index ecf4da8..09939bf 100644
--- a/README.org
+++ b/README.org
@@ -1,6 +1,4 @@
 * Mechanization of decidable type conversion with surjective pairing
-[[https://woodpecker.electriclam.com/api/badges/3/status.svg]]
-
 This repository contains a mechanized proof of decidable type
 conversion for a dependent type theory with a cumulative universe
 hierarchy, subtyping (contravariant on functions), natural numbers