equal
deleted
inserted
replaced
103 }) |
103 }) |
104 |
104 |
105 |
105 |
106 /* progress */ |
106 /* progress */ |
107 |
107 |
108 class Log_Progress extends Program_Progress(default_program = "build") { |
108 class Log_Progress extends Program_Progress(default_title = "build") { |
109 progress => |
109 progress => |
110 |
110 |
111 override def detect_program(s: String): Option[String] = |
111 override def detect_program(s: String): Option[String] = |
112 Document_Build.detect_program_start(s) |
112 Document_Build.detect_program_start(s) |
113 |
113 |