$EXTRA_HEAD = "<link rel=\"icon\" href=\"http://maxima.sourceforge.net/favicon.ico\"/>"