summaryrefslogtreecommitdiff
path: root/INSTALL
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-12-17 12:40:50 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-12-17 17:12:57 -0500
commit464bbe3b057bde32b9e0e1aa1f989818dba585db (patch)
treeed9557aaa18b744bcc1766668d42534ff3f6d402 /INSTALL
parent6b0e8bdbe37c3a04ba43fb379270df4726502a63 (diff)
some config changes: new --bsd option, readline gives warning, default build is now production.
Diffstat (limited to 'INSTALL')
-rw-r--r--INSTALL7
1 files changed, 6 insertions, 1 deletions
diff --git a/INSTALL b/INSTALL
index f0e1f6cc6..d8634f3e8 100644
--- a/INSTALL
+++ b/INSTALL
@@ -126,7 +126,12 @@ GLPK.
The GNU Readline library is optionally used to provide command
editing, tab completion, and history functionality at the CVC prompt
(when running in interactive mode). Check your distribution for a
-package named "libreadline-dev" or "readline-devel" or similar.
+package named "libreadline-dev" or "readline-devel" or similar. This
+library is covered by the GNU General Public License, version 3. Like
+the above-mentioned libraries, if you choose to use CVC4 with readline
+support, you are licensing CVC4 under that same license. (Please visit
+http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more
+details about readline.)
The Boost C++ threading library (often packaged independently of the
Boost base library) is needed to run CVC4 in "portfolio"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback