# HG changeset patch
# User wenzelm
# Date 1515869437 -3600
# Node ID c4c8787ed66914e9bc0942cf20b406597c2f17b0
# Parent  866b1ad870acc982361f91e1cd570c3c1969d9dc
tuned;

diff -r 866b1ad870ac -r c4c8787ed669 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;