tuned: avoid warning in IntelliJ IDEA;
authorwenzelm
Wed, 02 Nov 2022 16:13:29 +0100
changeset 76407 7e1a72af970b
parent 76406 40a365360680
child 76408 2768a6d71570
tuned: avoid warning in IntelliJ IDEA;
src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Nov 02 11:34:24 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Nov 02 16:13:29 2022 +0100
@@ -367,7 +367,7 @@
 
   /* manager thread */
 
-  private val delay_prune =
+  private lazy val delay_prune =
     Delay.first(prune_delay) { manager.send(Prune_History) }
 
   private val manager: Consumer_Thread[Any] = {