From b77ff791333c04d81a1acba33bc0bb59dcf7c6d6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Sep 2022 19:02:12 -0700 Subject: [PATCH] fix: put `Lean.Server.FileWorker.WidgetRequests` back --- src/Lean/Server/FileWorker.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 07e2dd99f7..8babd5f130 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -22,7 +22,7 @@ import Lean.Server.References import Lean.Server.FileWorker.Utils import Lean.Server.FileWorker.RequestHandling - +import Lean.Server.FileWorker.WidgetRequests import Lean.Server.Rpc.Basic import Lean.Widget.InteractiveDiagnostic