Options script fix.

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 087af0ef62f60b3e68b356ff88324419bf4da3bb..32f81455b65750fa3de239eb169199839a6a59df 100755 (executable)
--- 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