function typo_guillemets_post_typo($texte) {
	// ...
	switch ($GLOBALS['spip_lang']) {
		case 'fr':
			$guilles="« $2 »"; //LRTEUIN
			break;
		// ...
	}

	// on echappe les " dans les tags ;
	// attention ici \01 est le caractere chr(1), et \$0 represente le tag
	$texte = preg_replace(',<[^>]*"[^>]*(>|$),msSe', "str_replace('\"','\01', \"\$0\")", $texte);

	// on corrige les guill restants, qui sont par definition hors des tags
	// Un guill n'est pas pris s'il suit un caractere autre que espace, ou
	// s'il est suivi par un caractere de mot (lettre, chiffre)
	$texte = preg_replace('/(^|\s)"\s?([^"]*?)\s?"(\W|$)/S', '$1'.$guilles.'$3', $texte);

	// et on remet les guill des tags
	return str_replace("\01", '"', $texte);
}