diff options
Diffstat (limited to 'src/options/mkoptions')
| -rwxr-xr-x | src/options/mkoptions | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/options/mkoptions b/src/options/mkoptions index a3a1571ec..03d7837ac 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -352,6 +352,10 @@ function handle_option { WARN "$internal is inaccessible via SmtEngine (no smt name for option) but can be set via command-line: $long_option $short_option $long_option_alternate $short_option_alternate" fi fi + # in options files, use an smt name of ":" to force there not to be one + if [ "$smtname" = : ]; then + smtname= + fi # check for duplicates if [ "$internal" != - ]; then |