DISCHARGE_JML_COMMENTS

Print the original jml comments, but discharge them, s.t. they are not interpreted anymore