# HG changeset patch
# User wenzelm
# Date 1667402009 -3600
# Node ID 7e1a72af970b1cd4513158c8518c7c2cf39b1ec5
# Parent  40a36536068022143326b879a7132c1f9345fee4
tuned: avoid warning in IntelliJ IDEA;

diff -r 40a365360680 -r 7e1a72af970b 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] = {