diff options
| author | Andrew V. Jones <andrew.jones@vector.com> | 2020-07-17 18:09:14 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-17 10:09:14 -0700 |
| commit | e8df6f67cc2654f50d49995377a4b411668235e1 (patch) | |
| tree | fb8c2b35197e5821ac15c78b74da0d2de8eec3fc /INSTALL.md | |
| parent | 0988217562006d3f59e01dc261f39121df6d75f5 (diff) | |
Support for using 'libedit' over 'readline' #4571 (#4579)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/INSTALL.md b/INSTALL.md index 2c73827c1..a5b048131 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -176,18 +176,12 @@ and-inverter-graphs (AIG) and ABC is used to simplify these AIGs. ABC can be installed using the `contrib/get-abc` script. Configure CVC4 with `configure.sh --abc` to build with this dependency. -### GNU Readline library (Improved Interactive Experience) +### Editline library (Improved Interactive Experience) -The [GNU Readline](http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html) -library is optionally used to provide command editing, tab completion, and -history functionality at the CVC4 prompt (when running in interactive mode). -Check your distribution for a package named "libreadline-dev" or -"readline-devel" or similar. - -Note that GNU Readline is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html). -If you choose to use CVC4 with GNU Readline support, you are licensing CVC4 -under that same license. -(Usually CVC4's license is more permissive; see above discussion.) +The [Editline Library](https://thrysoee.dk/editline/) library is optionally +used to provide command editing, tab completion, and history functionality at +the CVC4 prompt (when running in interactive mode). Check your distribution +for a package named "libedit-dev" or "libedit-devel" or similar. ### Boost C++ base libraries (Examples) |