changeset 59720 | f893472fff31 |
parent 59366 | e94df7f6b608 |
child 61590 | 94ab348eaab2 |
--- a/src/Pure/Tools/print_operation.scala Mon Mar 16 16:26:33 2015 +0100 +++ b/src/Pure/Tools/print_operation.scala Mon Mar 16 16:59:59 2015 +0100 @@ -1,4 +1,4 @@ -/* Title: Pure/System/print_operation.scala +/* Title: Pure/Tools/print_operation.scala Author: Makarius Print operations as asynchronous query.