From 8bd305270a83f8794859108b3e8eb200971a7521 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 8 Aug 2016 13:38:01 -0400 Subject: 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 --- lib/js/urweb.js | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib') 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 { -- cgit v1.2.3