function remove_comment(s) {
	return s.replace(/\/\*.*?(\*\/|$)/, '');
}