diff options
| author | Teddy Wing | 2018-11-15 08:18:35 +0100 |
|---|---|---|
| committer | Teddy Wing | 2018-11-15 16:49:33 +0100 |
| commit | e12f656eb9b692c11c0704421c51c59d7052c121 (patch) | |
| tree | 41444f173fbb7c034fc84e76da59851149ccc25f | |
| parent | e3f1aac1caada3efaac7819d101cee850181f0da (diff) | |
| download | DomeKey-e12f656eb9b692c11c0704421c51c59d7052c121.tar.bz2 | |
Makefile: Add man pages to `dist/` directory
| -rw-r--r-- | Makefile | 8 |
1 files changed, 7 insertions, 1 deletions
@@ -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 $< $@ |