From 1f48835b7252757bb778a93bdac2d62e1dea59bc Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 24 Sep 2012 18:37:22 +0000
Subject: Fix the memout issue seen in recent nightly regressions (was due to a
 Statistics-printing problem, limited to certain benchmarks).

Mark some unlabeled header files "cvc4_private.h".

Other minor cleanup.

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/options/base_options_handlers.h |  2 ++
 src/options/base_options_template.h | 12 +++++++-----
 src/options/mkoptions               |  2 --
 3 files changed, 9 insertions(+), 7 deletions(-)

(limited to 'src/options')

diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 66dc97808..f29e98a9b 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__BASE_OPTIONS_HANDLERS_H
 #define __CVC4__BASE_OPTIONS_HANDLERS_H
 
diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h
index 97c19930e..c613ff8fd 100644
--- a/src/options/base_options_template.h
+++ b/src/options/base_options_template.h
@@ -16,17 +16,19 @@
  ** Contains code for handling command-line options
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__OPTIONS__${module_id}_H
 #define __CVC4__OPTIONS__${module_id}_H
 
 #include "options/options.h"
 ${module_includes}
 
-#line 26 "${template}"
+#line 28 "${template}"
 
 ${module_optionholder_spec}
 
-#line 30 "${template}"
+#line 32 "${template}"
 
 namespace CVC4 {
 
@@ -34,19 +36,19 @@ namespace options {
 
 ${module_decls}
 
-#line 38 "${template}"
+#line 40 "${template}"
 
 }/* CVC4::options namespace */
 
 ${module_specializations}
 
-#line 44 "${template}"
+#line 46 "${template}"
 
 namespace options {
 
 ${module_inlines}
 
-#line 50 "${template}"
+#line 52 "${template}"
 
 }/* CVC4::options namespace */
 
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 9e5fb2b81..69d7643c7 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -810,7 +810,6 @@ function handle_alias {
       expect_arg_long=required_argument
       arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')"
       option="$(echo "$option" | sed 's,--,,;s,=.*,,')"
-      echo "warning: not yet handling long-option alias =$arg" >&2
     else
       expect_arg_long=no_argument
       arg=
@@ -831,7 +830,6 @@ function handle_alias {
       expect_arg=:
       arg="$(echo "$option" | sed 's,[^=]*=,,')"
       option="$(echo "$option" | sed 's,-\(.\)=.*,\1,')"
-      echo "warning: not yet handling short-option alias =$arg" >&2
     else
       expect_arg=
       arg=
-- 
cgit v1.2.3