tuned;
authorwenzelm
Sat, 13 Jan 2018 19:50:37 +0100
changeset 67420 c4c8787ed669
parent 67419 866b1ad870ac
child 67421 c4a10621c72e
tuned;
src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Jan 13 15:49:59 2018 +0100
+++ b/src/Pure/Thy/present.ML	Sat Jan 13 19:50:37 2018 +0100
@@ -191,7 +191,7 @@
   let
     val script =
       "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
-        " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
+        " -n " ^ Bash.string name ^ (if tags = "" then "" else " -t " ^ Bash.string tags);
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;