author | wenzelm |
Wed, 11 Nov 2020 21:09:56 +0100 | |
changeset 72577 | 77b51733ffdf |
parent 72576 | 913407dad883 |
child 72578 | 3e8395f9093a |
--- a/src/Pure/Thy/present.scala Wed Nov 11 21:06:52 2020 +0100 +++ b/src/Pure/Thy/present.scala Wed Nov 11 21:09:56 2020 +0100 @@ -283,8 +283,6 @@ // prepare document - List("log", "blg").foreach(ext => (doc_dir + Path.explode(root).ext(ext)).file.delete) - val result = if ((doc_dir + Path.explode("build")).is_file) { bash("./build pdf " + Bash.string(doc_name))