| Index: client/dom/scripts/dartdomgenerator.py
|
| diff --git a/client/dom/scripts/dartdomgenerator.py b/client/dom/scripts/dartdomgenerator.py
|
| index 4e8bc2a6a3fd8a77e6e45a747219dde0aa3f3e19..0186f1b10895281b69a1532b62247a20f5dd5586 100755
|
| --- a/client/dom/scripts/dartdomgenerator.py
|
| +++ b/client/dom/scripts/dartdomgenerator.py
|
| @@ -31,7 +31,7 @@ _webkit_renames = {
|
|
|
| _webkit_renames_inverse = dict((v,k) for k, v in _webkit_renames.iteritems())
|
|
|
| -def GenerateDOM(output_dir):
|
| +def GenerateDOM(native, output_dir):
|
| # TODO(sra): Make this entry point also generate HTML.
|
| current_dir = os.path.dirname(__file__)
|
|
|
| @@ -79,19 +79,22 @@ def GenerateDOM(output_dir):
|
| source_filter = ['WebKit', 'Dart'],
|
| super_database = common_database,
|
| common_prefix = 'common',
|
| - super_map = _webkit_renames_inverse)
|
| + super_map = _webkit_renames_inverse,
|
| + native = native)
|
|
|
| generator.Flush()
|
|
|
| - # Install default DOM library.
|
| - default = os.path.join(output_dir, DOM_DEFAULT_LIBRARY)
|
| - target = os.path.join(output_dir, DOM_LIBRARY)
|
| - shutil.copyfile(default, target)
|
| -
|
| def main():
|
| current_dir = os.path.dirname(__file__)
|
| + output_dir = os.path.join(current_dir, '..')
|
| +
|
| logging.config.fileConfig(os.path.join(current_dir, 'logging.conf'))
|
| - GenerateDOM(os.path.join(current_dir, '..'))
|
| + GenerateDOM(False, output_dir)
|
| +
|
| + # Install default DOM library.
|
| + default = os.path.join(output_dir, DOM_DEFAULT_LIBRARY)
|
| + target = os.path.join(output_dir, DOM_LIBRARY)
|
| + shutil.copyfile(default, target)
|
|
|
| if __name__ == '__main__':
|
| sys.exit(main())
|
|
|