# HG changeset patch
# User wenzelm
# Date 1675192143 -3600
# Node ID 158dfe7f68ed3654774544187528036e0b137df7
# Parent  b899d7840b49da8397141cbea3399fab07061b75
clarified GUI events;

diff -r b899d7840b49 -r 158dfe7f68ed src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 19:50:58 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 20:09:03 2023 +0100
@@ -301,7 +301,9 @@
       tooltip = Word.capitalize(document_auto.description)
       override def clicked(state: Boolean): Unit = {
         super.clicked(state)
+
         if (state) delay_auto_build.invoke()
+        else delay_auto_build.revoke()
       }
     }