diff options
Diffstat (limited to 'src/options/printer_modes.h')
| -rw-r--r-- | src/options/printer_modes.h | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h index 09395dd5e..d4cdbd9a4 100644 --- a/src/options/printer_modes.h +++ b/src/options/printer_modes.h @@ -27,7 +27,7 @@ namespace options { /** Enumeration of inst_format modes (how to print models from get-model * command). */ -enum class CVC4_PUBLIC InstFormatMode +enum class InstFormatMode { /** default mode (print expressions in the output language format) */ DEFAULT, @@ -37,8 +37,7 @@ enum class CVC4_PUBLIC InstFormatMode } // namespace options -std::ostream& operator<<(std::ostream& out, - options::InstFormatMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, options::InstFormatMode mode); } // namespace CVC4 |