write_identifier


Description:

private void write_identifier (string s)