aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2016-10-24 15:30:21 +0200
committerGitHub <noreply@github.com>2016-10-24 15:30:21 +0200
commitbcb2b7b76272d63b3704bbdc76b9125a0b581bb8 (patch)
tree05376ce77761d218d5613d3aa6fd635bb1495c6c /Makefile
parentdfdc844ee7b08fda327798350125b6e79727dc27 (diff)
parent3599d11a6e20225f68dc29c997b5d4d987b10531 (diff)
downloadcompcert-bcb2b7b76272d63b3704bbdc76b9125a0b581bb8.tar.gz
compcert-bcb2b7b76272d63b3704bbdc76b9125a0b581bb8.zip
Merge pull request #147 from m-schmidt/master
Add a man page
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 2d16da42..ceb8109c 100644
--- a/Makefile
+++ b/Makefile
@@ -230,6 +230,8 @@ install:
install -m 0755 ./ccomp $(BINDIR)
install -d $(SHAREDIR)
install -m 0644 ./compcert.ini $(SHAREDIR)
+ install -d $(MANDIR)/man1
+ install -m 0644 ./doc/ccomp.1 $(MANDIR)/man1
$(MAKE) -C runtime install
ifeq ($(CLIGHTGEN),true)
install -m 0755 ./clightgen $(BINDIR)