--- web/site.cd 2007/07/10 17:29:02 369 +++ web/site.cd 2007/07/10 17:29:11 370 @@ -74,9 +74,11 @@ (* Highlighting text between {{...}} *) -let fun highlight (String -> [ (Char | Xvar)* ] ) +let fun highlight (String -> [ (Char | Xvar | Xi)* ] ) | [ '{{' h ::(Char *?) '}}' ; rest ] -> [ h; highlight rest ] + | [ '{/{' h ::(Char *?) '}}' ; rest ] -> + [ h; highlight rest ] | [ c; rest ] -> [ c; highlight rest ] | [] -> [];; @@ -270,7 +272,7 @@ [ '' !(patch_css (print_xml html)) ] in - dump_to_file (name @ ".html.php") txt;; + dump_to_file (name @ (if php then ".html.php" else ".html")) txt;; let fun gen_page_seq (prev : Page|[], pages : [Page*], next : Page|[],