From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 9 Jul 2012 20:13:23 +0000 (+0000)
Subject: minor fix-ups
X-Git-Tag: cvc5-1.0.0~7940
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42e7a38f0a0b38722c2f58ff028a5d3af9337347;p=cvc5.git

minor fix-ups
---

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"
 
diff --git a/doc/cvc4.1.in b/doc/cvc4.1.in
index dfc7e01a0..6c6a9768c 100644
--- a/doc/cvc4.1.in
+++ b/doc/cvc4.1.in
@@ -3,17 +3,26 @@
 .\"
 .TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals"
 .SH NAME
-cvc4 \- an automated theorem prover
+cvc4, pcvc4 \- an automated theorem prover
 .SH SYNOPSIS
 .B cvc4 [
 .I options
 .B ] [
 .I file
 .B ]
+.P
+.B pcvc4 [
+.I options
+.B ] [
+.I file
+.B ]
 .SH DESCRIPTION
 .B cvc4
 is an automated theorem prover for first-order formulas with respect
 to background theories of interest.
+.B pcvc4
+is CVC4's "portfolio" variant, which is capable of running multiple
+CVC4 instances in parallel, configured differently.
 
 With
 .I file