# HG changeset patch
# User wenzelm
# Date 1675287542 -3600
# Node ID 0f77e50eb87016ec333bf4a4ea16a8dd0aa8b071
# Parent  dad9960852a268ada5829ba361eb500fe91a47ed
clarified messages, notably for session "Intro";

diff -r dad9960852a2 -r 0f77e50eb870 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Feb 01 21:29:35 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Feb 01 22:39:02 2023 +0100
@@ -325,6 +325,10 @@
       session_graph.write(doc_dir)
 
       progress.bash("ls -alR", echo = true, cwd = doc_dir.file).check
+      progress match {
+        case program_progress: Program_Progress => program_progress.stop_program()
+        case _ =>
+      }
 
       Directory(doc_dir, doc, root_name, sources)
     }