diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-18 15:41:02 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-18 15:41:34 -0400 |
| commit | b2981aca1caaaa06605226296377fcd7a2d6f6d3 (patch) | |
| tree | 67d77d6c769d2897f0c691f596caf17474c0808a /src/options/mkoptions | |
| parent | 4ca5ef47c46c8e26b23e881bdd6faad848413f75 (diff) | |
Options script fix.
Diffstat (limited to 'src/options/mkoptions')
| -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 |