Remove `Options::wasSetByUser()` (#6682)

This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 048f5d06b..b733f62ce 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -135,12 +135,12 @@ Printer* Printer::getPrinter(OutputLanguage lang)
     // the singleton "null" expr.  So we guard against segfault
     if (not Options::isCurrentNull())
     {
-      if (Options::current().wasSetByUser(options::outputLanguage))
+      if (Options::current().base.outputLanguageWasSetByUser)
       {
         lang = options::outputLanguage();
       }
       if (lang == language::output::LANG_AUTO
-          && Options::current().wasSetByUser(options::inputLanguage))
+          && Options::current().base.inputLanguageWasSetByUser)
       {
         lang = language::toOutputLanguage(options::inputLanguage());
       }