clarified messages, notably for session "Intro";
authorwenzelm
Wed, 01 Feb 2023 22:39:02 +0100
changeset 77176 0f77e50eb870
parent 77175 dad9960852a2
child 77177 76180e429491
clarified messages, notably for session "Intro";
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)
     }