copy_files *.sty;
authorwenzelm
Thu, 24 Jan 2002 22:44:10 +0100
changeset 12849 b5824b740d05
parent 12848 ac191fb20ff1
child 12850 d3c16021e999
copy_files *.sty;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Jan 24 22:43:40 2002 +0100
+++ b/src/Pure/Thy/present.ML	Thu Jan 24 22:44:10 2002 +0100
@@ -355,7 +355,8 @@
       else None;
 
     fun doc_common path =
-      ((case opt_graphs of None => () | Some (pdf, eps) =>
+      (copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
+      (case opt_graphs of None => () | Some (pdf, eps) =>
         (File.write (Path.append path graph_pdf_path) pdf;
           File.write (Path.append path graph_eps_path) eps));
       write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
@@ -390,7 +391,6 @@
 
     (case doc_prefix2 of None => () | Some path =>
      (File.mkdir path;
-      copy_files (Path.unpack "~~/lib/texinputs/*.sty") path;
       doc_common path;
       conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n"))));