From d028dd65e4daf269386ea788edd25f2f11b41f26 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 18 Mar 2019 14:54:47 -0700
Subject: [PATCH] disable the args dump

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/shell/main.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 1718e7314..9a21435fb 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -301,7 +301,7 @@ static void parse_cmd_line_args(int argc, char ** argv) {
 
 
 int STD_CALL main(int argc, char ** argv) {
-#ifdef DUMP_ARGS
+#ifdef DUMP_ARGS_
      std::cout << "args are: ";
      for (int i = 0; i < argc; i++)
          std::cout << argv[i] <<" ";