projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e6f4f9f) | patch
Remove output.h from public space, to avoid clashes with symbols defined in users...
authorMorgan Deters <mdeters@cs.nyu.edu>
Thu, 27 Jun 2013 19:35:24 +0000 (15:35 -0400)
committerMorgan Deters <mdeters@cs.nyu.edu>
Thu, 27 Jun 2013 20:46:22 +0000 (16:46 -0400)
commit38a13fe227e6b59a49509d4b5ae6618b4c14937a
treee81fb31b46ffc1e948c48d647ca7d2bc2467a211tree
parente6f4f9fbd3e2e3471f0df46959e3924368f31bdbcommit | diff
Remove output.h from public space, to avoid clashes with symbols defined in users' space.

Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's
not installed on users' machines, and public headers should not include it.

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
src/compat/cvc3_compat.cpp diff | blob | history
src/include/cvc4_private_library.h diff | blob | history
src/main/interactive_shell.cpp diff | blob | history
src/parser/antlr_input.h diff | blob | history
src/parser/antlr_line_buffered_input.cpp diff | blob | history
src/util/datatype.h diff | blob | history
src/util/dump.h diff | blob | history
src/util/output.h diff | blob | history
test/unit/expr/expr_public.h diff | blob | history
test/unit/expr/type_cardinality_public.h diff | blob | history