# HG changeset patch
# User wenzelm
# Date 1513097639 -3600
# Node ID 26f548370e8d20d67e9d9c3462c5a71f61763358
# Parent  9ab34bb83a840ce3d58bd2790a37684ac149bdd2
purge more thoroughly;

diff -r 9ab34bb83a84 -r 26f548370e8d src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Dec 12 17:46:22 2017 +0100
+++ b/src/Pure/Thy/present.ML	Tue Dec 12 17:53:59 2017 +0100
@@ -194,11 +194,12 @@
       "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
         " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
+    val _ = if purge then Isabelle_System.rm_tree dir else ();
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;
     val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
     val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
-    val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
+    val _ = if purge then Isabelle_System.rm_tree dir else ();
   in doc_path end;