# Append an entry for the doc in the given infobox
	private fun add_doc_to_infobox(res: HInfoBox)
	do
		var mdoc = mdoc_or_fallback
		if mdoc != null then mdoc.fill_infobox(res)
	end