doc: Should have been removed earlier but Git doesn't track empty directories and I failed to git mv.