diff options
author | Fabio Alessandrelli <fabio.alessandrelli@gmail.com> | 2021-01-25 16:24:26 +0100 |
---|---|---|
committer | Fabio Alessandrelli <fabio.alessandrelli@gmail.com> | 2021-01-25 17:47:52 +0100 |
commit | abb8d8e8ca75b8aaa614f768bebed41ad88ff39f (patch) | |
tree | 088096929106d7b9c3823fe8ca48944bd83c256c | |
parent | 2ea7592ca18f66ab29cd4212772c1c339ed22018 (diff) |
[HTML5] Fix "initial_memory" build option parsing
-rw-r--r-- | platform/javascript/detect.py | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/platform/javascript/detect.py b/platform/javascript/detect.py index 0d57f8aad1..d8e3c61798 100644 --- a/platform/javascript/detect.py +++ b/platform/javascript/detect.py @@ -51,8 +51,11 @@ def get_flags(): def configure(env): if not isinstance(env["initial_memory"], int): - print("Initial memory must be a valid integer") - sys.exit(255) + try: + env["initial_memory"] = int(env["initial_memory"]) + except: + print("Initial memory must be a valid integer") + sys.exit(255) ## Build type |