diff options
| author | Teddy Wing | 2020-08-06 00:26:54 +0200 | 
|---|---|---|
| committer | Teddy Wing | 2020-08-06 00:26:54 +0200 | 
| commit | 1679cca32210b741677ef9cf48839cd951980cd9 (patch) | |
| tree | 05cddb1cae642c6053f704a6beaa2ac1ea890260 | |
| parent | 16ff238363973e980201f441a802308257c382b0 (diff) | |
| download | git-suggestion-1679cca32210b741677ef9cf48839cd951980cd9.tar.bz2 | |
Makefile: Put distribution man pages in `dist/share/man/man1/`
| -rw-r--r-- | Makefile | 7 | 
1 files changed, 5 insertions, 2 deletions
| @@ -45,8 +45,11 @@ dist: $(DIST_PRODUCTS) $(DIST_MAN_PAGES)  $(DIST):  	mkdir -p $@ +$(DIST)/share/man/man1: $(DIST) +	mkdir -p $@ +  $(DIST_PRODUCTS): $(DIST) $(RELEASE_PRODUCTS)  	cp $(RELEASE_PRODUCTS) $(DIST) -$(DIST_MAN_PAGES): $(DIST) $(MAN_PAGES) -	cp $(MAN_PAGES) $(DIST) +$(DIST_MAN_PAGES): $(DIST)/share/man/man1 $(MAN_PAGES) +	cp $(MAN_PAGES) $< | 
