+
+ OutputFont();
+}
+
+void HTMLHead()
+{
+ TexOutput("<head>");
+ if (htmlStylesheet) {
+ TexOutput("<link rel=stylesheet type=\"text/css\" href=\"");
+ TexOutput(htmlStylesheet);
+ TexOutput("\">");
+ }
+};
+
+void HTMLHeadTo(FILE* f)
+{
+ if (htmlStylesheet)
+ fprintf(f,"<head><link rel=stylesheet type=\"text/css\" href=\"%s\">",htmlStylesheet);
+ else
+ fprintf(f,"<head>");