--- a/src/Pure/Admin/build_doc.scala Sat Oct 15 11:26:31 2016 +0200
+++ b/src/Pure/Admin/build_doc.scala Sat Oct 15 11:38:03 2016 +0200
@@ -50,14 +50,14 @@
Build.build(
options.bool.update("browser_info", false).
string.update("document", "pdf").
- string.update("document_output", File.standard_path(output)),
+ string.update("document_output", output.implode),
progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode,
sessions = sessions)
if (res2.ok) {
- val doc_dir = Path.explode("$ISABELLE_HOME/doc").file
+ val doc_dir = Path.explode("$ISABELLE_HOME/doc")
for (doc <- selected_docs) {
- val name = doc + ".pdf"
- File.copy(new JFile(output, name), new JFile(doc_dir, name))
+ val name = Path.explode(doc + ".pdf")
+ File.copy(output + name, doc_dir + name)
}
}
res2.rc