equal
deleted
inserted
replaced
157 val forkedN: string val forked: T |
157 val forkedN: string val forked: T |
158 val joinedN: string val joined: T |
158 val joinedN: string val joined: T |
159 val runningN: string val running: T |
159 val runningN: string val running: T |
160 val finishedN: string val finished: T |
160 val finishedN: string val finished: T |
161 val failedN: string val failed: T |
161 val failedN: string val failed: T |
|
162 val consolidatedN: string val consolidated: T |
162 val exec_idN: string |
163 val exec_idN: string |
163 val initN: string |
164 val initN: string |
164 val statusN: string val status: T |
165 val statusN: string val status: T |
165 val resultN: string val result: T |
166 val resultN: string val result: T |
166 val writelnN: string val writeln: T |
167 val writelnN: string val writeln: T |
553 val (forkedN, forked) = markup_elem "forked"; |
554 val (forkedN, forked) = markup_elem "forked"; |
554 val (joinedN, joined) = markup_elem "joined"; |
555 val (joinedN, joined) = markup_elem "joined"; |
555 val (runningN, running) = markup_elem "running"; |
556 val (runningN, running) = markup_elem "running"; |
556 val (finishedN, finished) = markup_elem "finished"; |
557 val (finishedN, finished) = markup_elem "finished"; |
557 val (failedN, failed) = markup_elem "failed"; |
558 val (failedN, failed) = markup_elem "failed"; |
|
559 val (consolidatedN, consolidated) = markup_elem "consolidated"; |
558 |
560 |
559 |
561 |
560 (* messages *) |
562 (* messages *) |
561 |
563 |
562 val exec_idN = "exec_id"; |
564 val exec_idN = "exec_id"; |