From e12f656eb9b692c11c0704421c51c59d7052c121 Mon Sep 17 00:00:00 2001
From: Teddy Wing
Date: Thu, 15 Nov 2018 08:18:35 +0100
Subject: Makefile: Add man pages to `dist/` directory

---
 Makefile | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 5d0beb4..806c533 100644
--- a/Makefile
+++ b/Makefile
@@ -109,10 +109,16 @@ doc/dome-key-mappings.7: doc/dome-key-mappings.7.txt
 # Distribution
 
 .PHONY: dist-all
-dist-all: dist/dome-key
+dist-all: dist/dome-key dist/dome-key.1 dist/dome-key-mappings.7
 
 dist:
 	mkdir -p dist
 
 dist/dome-key: $(ARCHIVE_PRODUCT) dist
 	cp $< $@
+
+dist/dome-key.1: doc/dome-key.1 dist
+	cp $< $@
+
+dist/dome-key-mappings.7: doc/dome-key-mappings.7 dist
+	cp $< $@
-- 
cgit v1.2.3