summaryrefslogtreecommitdiff
path: root/Makefile.am
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-07-09 20:13:23 +0000
committerMorgan Deters <mdeters@gmail.com>2012-07-09 20:13:23 +0000
commit42e7a38f0a0b38722c2f58ff028a5d3af9337347 (patch)
tree5f9dac3afecc40138b6f98d7db7425db792e93ab /Makefile.am
parent95ff2500c189a1c6a2dc6a6b29b1e8f9e792ac1d (diff)
minor fix-ups
Diffstat (limited to 'Makefile.am')
-rw-r--r--Makefile.am5
1 files changed, 5 insertions, 0 deletions
diff --git a/Makefile.am b/Makefile.am
index 2edd33820..b72c71031 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -111,11 +111,16 @@ EXTRA_DIST = \
doc/libcvc4compat.3.in
man_MANS = \
doc/cvc4.1 \
+ doc/pcvc4.1 \
doc/cvc4.5 \
doc/libcvc4.3 \
doc/libcvc4parser.3 \
doc/libcvc4compat.3
+doc/pcvc4.1:
+ rm -f doc/pcvc4.1
+ $(LN_S) cvc4.1 doc/pcvc4.1
+
dist-hook:
cp -p "$(srcdir)/Makefile" "$(distdir)/Makefile"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback