diff options
Diffstat (limited to 'src/jsifier.js')
| -rw-r--r-- | src/jsifier.js | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/jsifier.js b/src/jsifier.js index c4235b3f..86c9270e 100644 --- a/src/jsifier.js +++ b/src/jsifier.js @@ -222,7 +222,10 @@ function JSify(data) { function getLabelLines(label, indent) { var ret = ''; if (LABEL_DEBUG) { - ret += indent + " print(INDENT + '" + func.ident + ":" + label.ident + "');\n"; + ret += indent + "print(INDENT + '" + func.ident + ":" + label.ident + "');\n"; + } + if (EXECUTION_TIMEOUT > 0) { + ret += indent + 'if (Date.now() - START_TIME >= ' + (EXECUTION_TIMEOUT*1000) + ') throw "Timed out!" + (new Error().stack);\n'; } // for special labels we care about (for phi), mark that we visited them if (func.remarkableLabels.indexOf(label.ident) >= 0) { |