HTML_quoting      640 htags/src2html.c 	const char *quoted = HTML_quoting(c);
HTML_quoting      891 htags/src2html.c 			detab_replacing(out, _, HTML_quoting);