diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 206607911b..7a56426c40 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1757,6 +1757,14 @@ The constraints on the internal level of the occurrences of {\Type} {\tt Print Universes.} \end{quote} +This command also accepts an optional output filename: +\begin{quote} +\tt Print Universes {\str}. +\end{quote} +If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are +printed in the DOT language, and can be processed by Graphviz +tools. The format is unspecified if {\str} doesn't end in +\texttt{.dot} or \texttt{.gv}. %%% Local Variables: %%% mode: latex |