From 986e0c421b5c9dd564dbb0b9bf1e6606e34765d7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Aug 2024 16:27:11 -0700 Subject: [PATCH] [js] Set up workers earlier to avoid "Error: currentWorker is undefined:" --- fiat-html/main.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/fiat-html/main.js b/fiat-html/main.js index b173b459c0..85bf95ce9b 100644 --- a/fiat-html/main.js +++ b/fiat-html/main.js @@ -304,6 +304,8 @@ document.addEventListener('DOMContentLoaded', function() { wasmCheckbox.checked = true; } + setupWorkers(); + if (argv) { if (nonFalseQueryParam(interactive)) { inputArgs.value = decodeURIComponent(argv); @@ -314,8 +316,6 @@ document.addEventListener('DOMContentLoaded', function() { } else { inputForm.classList.remove('hidden'); } - - setupWorkers(); } parseQueryParams();