From bae7d1c9ad2d12a63b3bc7976e60e6c2a70d9613 Mon Sep 17 00:00:00 2001 From: Fons van der Plas Date: Tue, 19 Sep 2023 14:01:11 +0200 Subject: [PATCH] tiny type fix --- frontend/components/Editor.js | 1 - 1 file changed, 1 deletion(-) diff --git a/frontend/components/Editor.js b/frontend/components/Editor.js index 99bcc2369f..fe2ad5a6a7 100644 --- a/frontend/components/Editor.js +++ b/frontend/components/Editor.js @@ -847,7 +847,6 @@ patch: ${JSON.stringify( // https://github.com/fonsp/Pluto.jl/issues/2398 open_pluto_popup({ type: "warn", - source_element: null, body: html`

A new server was started - this notebook session is no longer running.

Would you like to go back to the main menu?