max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: put Lean.Server.FileWorker.WidgetRequests back

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-15 19:02:12 -07:00
parent c16d4fb926
commit b77ff79133
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/FileWorker.lean
View file

@ -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