diff -r 90c625edaee1 -r 0417e7ed93fd src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Mon Apr 12 23:51:00 2004 +0200 +++ b/src/Pure/Thy/present.ML Mon Apr 12 23:52:15 2004 +0200 @@ -375,12 +375,10 @@ if length path > 1 then update_index parent_html_prefix name else (); (case readme of None => () | Some path => File.copy path (Path.append html_prefix path)); write_graph graph (Path.append html_prefix graph_path); - copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class") - (Path.append html_prefix (Path.basic "awtUtilities")); - copy_files (Path.unpack "~~/lib/browser/GraphBrowser/*.class") - (Path.append html_prefix (Path.basic "GraphBrowser")); + copy_files (Path.unpack "~~/lib/browser/GraphBrowser.jar") html_prefix; seq (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) (HTML.applet_pages name (Url.file index_path, name)); + copy_files (Path.unpack "~~/lib/html/isabelle.css") html_prefix; seq finish_html thys; seq (uncurry File.write) files; conditional verbose (fn () =>