| Index: client/dom/scripts/dartdomgenerator.py
|
| diff --git a/client/dom/scripts/dartdomgenerator.py b/client/dom/scripts/dartdomgenerator.py
|
| index 7d8337e63b1a36e2b5cc617e4ab5cd808e797868..0a39819bb07321f9bf720c121094fbc132599a52 100755
|
| --- a/client/dom/scripts/dartdomgenerator.py
|
| +++ b/client/dom/scripts/dartdomgenerator.py
|
| @@ -162,7 +162,7 @@ def main():
|
| default=None,
|
| help='Directory to put the generated files')
|
| parser.add_option('--use-database-cache', dest='use_database_cache',
|
| - action='store',
|
| + action='store_true',
|
| default=False,
|
| help='''Use the cached database from the previous run to
|
| improve startup performance''')
|
|
|