Fix bug wherein #<void> gets printed in the output file.