# HG changeset patch
# User wenzelm
# Date 1674919618 -3600
# Node ID a2ae6baa82195419acf8f19784531bcabb87d435
# Parent  25a497bb7b0b04bf6b781ffa9f8e9a77aa6c8d3c
tuned comments;

diff -r 25a497bb7b0b -r a2ae6baa8219 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Sat Jan 28 16:20:44 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Sat Jan 28 16:26:58 2023 +0100
@@ -146,6 +146,8 @@
   }
 
 
+  /* init */
+
   def init(
     other_settings: List[String] = init_components(),
     fresh: Boolean = false,