--- a/src/Pure/Tools/print_operation.scala Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/Tools/print_operation.scala Thu Aug 27 12:34:10 2020 +0200
@@ -38,6 +38,6 @@
true
}
- val functions = List(Markup.PRINT_OPERATIONS -> put)
+ override val functions = List(Markup.PRINT_OPERATIONS -> put)
}
}