src/HOL/ex/ROOT.ML
changeset 30179 c703c9368c12
parent 29808 b8b9d529663b
child 30374 7311a1546d85
     1.1 --- a/src/HOL/ex/ROOT.ML	Sat Feb 28 20:29:20 2009 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Sat Feb 28 21:34:33 2009 +0100
     1.3 @@ -93,4 +93,5 @@
     1.4    use_thy "Sudoku"
     1.5  else ();
     1.6  
     1.7 -HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
     1.8 +HTML.with_charset "utf-8" (no_document use_thys)
     1.9 +  ["Hebrew", "Chinese", "Serbian"];