Fix comment note

diff --git a/base/main.cc b/base/main.cc
index 7530ec3075834445f4f37758117d4aaeef206172..cb8a7a7fe1524c9592e0e74c1b03d46eff04e910 100644 (file)
--- a/base/main.cc
+++ b/base/main.cc
@@ -97,7 +97,7 @@ int main()
 #if JSONLOGEDGES > 0
         p.logr(p.root());
 #endif
-#else // USE_INTERRUPT
+#else // NOT USE_INTERRUPT
         while(!p.goal_found()) {
                 p.tstart();
                 p.tend();