From 58b07681d667ae70e262b728555b75a2fdec8c6f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 18 Jun 2014 15:41:02 -0400
Subject: [PATCH] Options script fix.

---
 src/options/mkoptions | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 087af0ef6..32f81455b 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -2,7 +2,7 @@
 #
 # mkoptions
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2011-2013  The CVC4 Project
+# Copyright (c) 2011-2014  The CVC4 Project
 #
 # The purpose of this script is to create options.{h,cpp}
 # from template files and a list of options.
@@ -1478,7 +1478,7 @@ EOF
   fi
 }
 
-total=$(($#/2+21*${#templates[@]}))
+total=$(($#/2+23*${#templates[@]}))
 count=0
 while [ $# -gt 0 ]; do
   kf="$1"; shift
-- 
2.30.2