1 files changed, 1 insertions, 1 deletions
diff --git a/src/printer/printer.h b/src/printer/printer.h
index fcc0df93c..44e5ac9f4 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -62,7 +62,7 @@ public:
       //
       // Options can be null in certain circumstances (e.g., when printing
       // the singleton "null" expr.  So we guard against segfault
-      if(&Options::current() != NULL) {
+      if(not Options::isCurrentNull()) {
         if(options::outputLanguage.wasSetByUser()) {
           lang = options::outputLanguage();
         }