+# Restore stdout, and print the header plus whatever the plugins
+# produced if they produced anything. If they didn't, we avoid
+# printing the header.
+$stdout = STDOUT
+if output_buffer.size > 0 then
+ puts make_header(plugin_class.to_s())
+ puts output_buffer.string()