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