diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-06-02 08:55:24 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 06:55:24 +0000 |
| commit | 4dacf3183d6790ebb4615263908da294e43e3cb6 (patch) | |
| tree | 2b2b191c3bc5ad3bfd9967d83e22b1158aed4930 /src/options/printer_modes.h | |
| parent | 444487219984b510bfe8c95c25fd8d28466551d5 (diff) | |
Make `Options::assign()` specializations free functions (#6648)
This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions.
Diffstat (limited to 'src/options/printer_modes.h')
| -rw-r--r-- | src/options/printer_modes.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h index e27cb133f..093bff7d9 100644 --- a/src/options/printer_modes.h +++ b/src/options/printer_modes.h @@ -36,9 +36,9 @@ enum class InstFormatMode SZS, }; -} // namespace options +std::ostream& operator<<(std::ostream& out, InstFormatMode mode); -std::ostream& operator<<(std::ostream& out, options::InstFormatMode mode); +} // namespace options } // namespace cvc5 |