summaryrefslogtreecommitdiff
path: root/INSTALL
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-12-17 17:14:45 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-12-17 17:14:45 -0500
commitf411ca8ce97f488fd0db0a79abe8b4e61521ae69 (patch)
tree4112cd96e30928f4b57787eabe98a0aaa178540e /INSTALL
parent5186ca79710fe935d1f7ed27c4a34e913ab547e8 (diff)
parent464bbe3b057bde32b9e0e1aa1f989818dba585db (diff)
Merge branch '1.3.x'
Conflicts: COPYING NEWS
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