diff options
author | Adam Chlipala <adamc@csail.mit.edu> | 2016-08-08 13:38:01 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@csail.mit.edu> | 2016-08-08 13:38:01 -0400 |
commit | 8bd305270a83f8794859108b3e8eb200971a7521 (patch) | |
tree | 1ee870ecf871f21eb5aaea70612c83917ac81177 /lib | |
parent | 06cb0a88e1df0d4c84427786a9d04f7a75856854 (diff) |
Avoid repopulating dead nodes; otherwise, we might wind up killing a node multiple times, screwing up the free list of available closure IDs (with duplicates), so that the same ID gets allocated for multiple functions later
Diffstat (limited to 'lib')
-rw-r--r-- | lib/js/urweb.js | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js index 68e7979d..b871b8e5 100644 --- a/lib/js/urweb.js +++ b/lib/js/urweb.js @@ -731,6 +731,8 @@ function flattenLocal(s) { // Dynamic tree management function populate(node) { + if (node.dead) return; + var s = node.signal; var oldSources = node.sources; try { |