write_newline


Description:

public void write_newline ()

Writes a newline.