changeset 37940 | 4857eab31298 |
parent 37939 | 965537d86fcc |
child 38133 | 987680d2e77d |
--- a/src/Pure/Thy/present.ML Thu Jul 22 22:31:20 2010 +0200 +++ b/src/Pure/Thy/present.ML Thu Jul 22 22:39:31 2010 +0200 @@ -466,7 +466,7 @@ val base = Path.base path; val base_html = html_ext base; val _ = add_file (Path.append html_prefix base_html, - HTML.ml_file (Url.File base) (File.read path)); + HTML.external_file (Url.File base) (File.read path)); in (Url.File base_html, Url.File raw_path, loadit) end); fun prep_html_source (tex_source, html_source, html) =