diff options
author | Dan Gohman <sunfish@google.com> | 2014-02-24 08:47:10 -0800 |
---|---|---|
committer | Dan Gohman <sunfish@google.com> | 2014-02-25 11:58:53 -0800 |
commit | de5271f3c1ffce1cd91496fddde37708662c92c8 (patch) | |
tree | 729cfe6000b08275b2df9129ac57cb7d9387a360 | |
parent | 3317f2cd793893073619a87a462da26c505ba9eb (diff) |
Fix the banned_js_engines mechanism.
-rw-r--r-- | tools/shared.py | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tools/shared.py b/tools/shared.py index e6be09d0..92186c2c 100644 --- a/tools/shared.py +++ b/tools/shared.py @@ -687,9 +687,12 @@ else: try: if 'gcparam' not in str(SPIDERMONKEY_ENGINE): + new_spidermonkey = SPIDERMONKEY_ENGINE if type(SPIDERMONKEY_ENGINE) is str: - SPIDERMONKEY_ENGINE = [SPIDERMONKEY_ENGINE] - SPIDERMONKEY_ENGINE += ['-e', "gcparam('maxBytes', 1024*1024*1024);"] # Our very large files need lots of gc heap + new_spidermonkey = [SPIDERMONKEY_ENGINE] + new_spidermonkey += ['-e', "gcparam('maxBytes', 1024*1024*1024);"] # Our very large files need lots of gc heap + JS_ENGINES = map(lambda x: x if x != SPIDERMONKEY_ENGINE else new_spidermonkey, JS_ENGINES) + SPIDERMONKEY_ENGINE = new_spidermonkey except NameError: pass |