diff options
Diffstat (limited to 'src/options')
-rwxr-xr-x | src/options/mkoptions | 4 |
1 files 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 |