5d2dfa9f40
An unfortunate side effect of switching from print to output() is that all output() goes to stderr. We should probably carefully consider whether this is the right thing to do.