<?php /// $Id$

$string['filtername'] = "Notation TeX";

?>